Proof of Theorem lnoadd
Step | Hyp | Ref
| Expression |
1 | | ax-1cn 9873 |
. . 3
⊢ 1 ∈
ℂ |
2 | | lnoadd.1 |
. . . 4
⊢ 𝑋 = (BaseSet‘𝑈) |
3 | | eqid 2610 |
. . . 4
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
4 | | lnoadd.5 |
. . . 4
⊢ 𝐺 = ( +𝑣
‘𝑈) |
5 | | lnoadd.6 |
. . . 4
⊢ 𝐻 = ( +𝑣
‘𝑊) |
6 | | eqid 2610 |
. . . 4
⊢ (
·𝑠OLD ‘𝑈) = ( ·𝑠OLD
‘𝑈) |
7 | | eqid 2610 |
. . . 4
⊢ (
·𝑠OLD ‘𝑊) = ( ·𝑠OLD
‘𝑊) |
8 | | lnoadd.7 |
. . . 4
⊢ 𝐿 = (𝑈 LnOp 𝑊) |
9 | 2, 3, 4, 5, 6, 7, 8 | lnolin 26993 |
. . 3
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (1 ∈ ℂ ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑇‘((1(
·𝑠OLD ‘𝑈)𝐴)𝐺𝐵)) = ((1(
·𝑠OLD ‘𝑊)(𝑇‘𝐴))𝐻(𝑇‘𝐵))) |
10 | 1, 9 | mp3anr1 1413 |
. 2
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑇‘((1(
·𝑠OLD ‘𝑈)𝐴)𝐺𝐵)) = ((1(
·𝑠OLD ‘𝑊)(𝑇‘𝐴))𝐻(𝑇‘𝐵))) |
11 | | simp1 1054 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑈 ∈ NrmCVec) |
12 | | simpl 472 |
. . . . 5
⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → 𝐴 ∈ 𝑋) |
13 | 2, 6 | nvsid 26866 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (1(
·𝑠OLD ‘𝑈)𝐴) = 𝐴) |
14 | 11, 12, 13 | syl2an 493 |
. . . 4
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (1(
·𝑠OLD ‘𝑈)𝐴) = 𝐴) |
15 | 14 | oveq1d 6564 |
. . 3
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((1(
·𝑠OLD ‘𝑈)𝐴)𝐺𝐵) = (𝐴𝐺𝐵)) |
16 | 15 | fveq2d 6107 |
. 2
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑇‘((1(
·𝑠OLD ‘𝑈)𝐴)𝐺𝐵)) = (𝑇‘(𝐴𝐺𝐵))) |
17 | | simpl2 1058 |
. . . 4
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → 𝑊 ∈ NrmCVec) |
18 | 2, 3, 8 | lnof 26994 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊)) |
19 | | ffvelrn 6265 |
. . . . 5
⊢ ((𝑇:𝑋⟶(BaseSet‘𝑊) ∧ 𝐴 ∈ 𝑋) → (𝑇‘𝐴) ∈ (BaseSet‘𝑊)) |
20 | 18, 12, 19 | syl2an 493 |
. . . 4
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑇‘𝐴) ∈ (BaseSet‘𝑊)) |
21 | 3, 7 | nvsid 26866 |
. . . 4
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑇‘𝐴) ∈ (BaseSet‘𝑊)) → (1(
·𝑠OLD ‘𝑊)(𝑇‘𝐴)) = (𝑇‘𝐴)) |
22 | 17, 20, 21 | syl2anc 691 |
. . 3
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (1(
·𝑠OLD ‘𝑊)(𝑇‘𝐴)) = (𝑇‘𝐴)) |
23 | 22 | oveq1d 6564 |
. 2
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → ((1(
·𝑠OLD ‘𝑊)(𝑇‘𝐴))𝐻(𝑇‘𝐵)) = ((𝑇‘𝐴)𝐻(𝑇‘𝐵))) |
24 | 10, 16, 23 | 3eqtr3d 2652 |
1
⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑇‘(𝐴𝐺𝐵)) = ((𝑇‘𝐴)𝐻(𝑇‘𝐵))) |