Proof of Theorem dvhvaddass
| Step | Hyp | Ref
| Expression |
| 1 | | coass 6285 |
. . . 4
⊢
(((1st ‘𝐹) ∘ (1st ‘𝐺)) ∘ (1st
‘𝐼)) =
((1st ‘𝐹)
∘ ((1st ‘𝐺) ∘ (1st ‘𝐼))) |
| 2 | | dvhvaddcl.h |
. . . . . . . . 9
⊢ 𝐻 = (LHyp‘𝐾) |
| 3 | | dvhvaddcl.t |
. . . . . . . . 9
⊢ 𝑇 = ((LTrn‘𝐾)‘𝑊) |
| 4 | | dvhvaddcl.e |
. . . . . . . . 9
⊢ 𝐸 = ((TEndo‘𝐾)‘𝑊) |
| 5 | | dvhvaddcl.u |
. . . . . . . . 9
⊢ 𝑈 = ((DVecH‘𝐾)‘𝑊) |
| 6 | | dvhvaddcl.d |
. . . . . . . . 9
⊢ 𝐷 = (Scalar‘𝑈) |
| 7 | | dvhvaddcl.a |
. . . . . . . . 9
⊢ + =
(+g‘𝑈) |
| 8 | | dvhvaddcl.p |
. . . . . . . . 9
⊢ ⨣ =
(+g‘𝐷) |
| 9 | 2, 3, 4, 5, 6, 7, 8 | dvhvadd 41094 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) = 〈((1st ‘𝐹) ∘ (1st
‘𝐺)),
((2nd ‘𝐹)
⨣
(2nd ‘𝐺))〉) |
| 10 | 9 | 3adantr3 1172 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) = 〈((1st ‘𝐹) ∘ (1st
‘𝐺)),
((2nd ‘𝐹)
⨣
(2nd ‘𝐺))〉) |
| 11 | 10 | fveq2d 6910 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (1st ‘(𝐹 + 𝐺)) = (1st
‘〈((1st ‘𝐹) ∘ (1st ‘𝐺)), ((2nd
‘𝐹) ⨣
(2nd ‘𝐺))〉)) |
| 12 | | fvex 6919 |
. . . . . . . 8
⊢
(1st ‘𝐹) ∈ V |
| 13 | | fvex 6919 |
. . . . . . . 8
⊢
(1st ‘𝐺) ∈ V |
| 14 | 12, 13 | coex 7952 |
. . . . . . 7
⊢
((1st ‘𝐹) ∘ (1st ‘𝐺)) ∈ V |
| 15 | | ovex 7464 |
. . . . . . 7
⊢
((2nd ‘𝐹) ⨣ (2nd
‘𝐺)) ∈
V |
| 16 | 14, 15 | op1st 8022 |
. . . . . 6
⊢
(1st ‘〈((1st ‘𝐹) ∘ (1st ‘𝐺)), ((2nd
‘𝐹) ⨣
(2nd ‘𝐺))〉) = ((1st ‘𝐹) ∘ (1st
‘𝐺)) |
| 17 | 11, 16 | eqtrdi 2793 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (1st ‘(𝐹 + 𝐺)) = ((1st ‘𝐹) ∘ (1st
‘𝐺))) |
| 18 | 17 | coeq1d 5872 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((1st ‘(𝐹 + 𝐺)) ∘ (1st ‘𝐼)) = (((1st
‘𝐹) ∘
(1st ‘𝐺))
∘ (1st ‘𝐼))) |
| 19 | 2, 3, 4, 5, 6, 7, 8 | dvhvadd 41094 |
. . . . . . . 8
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (𝐺 + 𝐼) = 〈((1st ‘𝐺) ∘ (1st
‘𝐼)),
((2nd ‘𝐺)
⨣
(2nd ‘𝐼))〉) |
| 20 | 19 | 3adantr1 1170 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (𝐺 + 𝐼) = 〈((1st ‘𝐺) ∘ (1st
‘𝐼)),
((2nd ‘𝐺)
⨣
(2nd ‘𝐼))〉) |
| 21 | 20 | fveq2d 6910 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (1st ‘(𝐺 + 𝐼)) = (1st
‘〈((1st ‘𝐺) ∘ (1st ‘𝐼)), ((2nd
‘𝐺) ⨣
(2nd ‘𝐼))〉)) |
| 22 | | fvex 6919 |
. . . . . . . 8
⊢
(1st ‘𝐼) ∈ V |
| 23 | 13, 22 | coex 7952 |
. . . . . . 7
⊢
((1st ‘𝐺) ∘ (1st ‘𝐼)) ∈ V |
| 24 | | ovex 7464 |
. . . . . . 7
⊢
((2nd ‘𝐺) ⨣ (2nd
‘𝐼)) ∈
V |
| 25 | 23, 24 | op1st 8022 |
. . . . . 6
⊢
(1st ‘〈((1st ‘𝐺) ∘ (1st ‘𝐼)), ((2nd
‘𝐺) ⨣
(2nd ‘𝐼))〉) = ((1st ‘𝐺) ∘ (1st
‘𝐼)) |
| 26 | 21, 25 | eqtrdi 2793 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (1st ‘(𝐺 + 𝐼)) = ((1st ‘𝐺) ∘ (1st
‘𝐼))) |
| 27 | 26 | coeq2d 5873 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((1st ‘𝐹) ∘ (1st
‘(𝐺 + 𝐼))) = ((1st
‘𝐹) ∘
((1st ‘𝐺)
∘ (1st ‘𝐼)))) |
| 28 | 1, 18, 27 | 3eqtr4a 2803 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((1st ‘(𝐹 + 𝐺)) ∘ (1st ‘𝐼)) = ((1st
‘𝐹) ∘
(1st ‘(𝐺
+ 𝐼)))) |
| 29 | | xp2nd 8047 |
. . . . . 6
⊢ (𝐹 ∈ (𝑇 × 𝐸) → (2nd ‘𝐹) ∈ 𝐸) |
| 30 | | xp2nd 8047 |
. . . . . 6
⊢ (𝐺 ∈ (𝑇 × 𝐸) → (2nd ‘𝐺) ∈ 𝐸) |
| 31 | | xp2nd 8047 |
. . . . . 6
⊢ (𝐼 ∈ (𝑇 × 𝐸) → (2nd ‘𝐼) ∈ 𝐸) |
| 32 | 29, 30, 31 | 3anim123i 1152 |
. . . . 5
⊢ ((𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸)) → ((2nd ‘𝐹) ∈ 𝐸 ∧ (2nd ‘𝐺) ∈ 𝐸 ∧ (2nd ‘𝐼) ∈ 𝐸)) |
| 33 | | eqid 2737 |
. . . . . . . . . 10
⊢
((EDRing‘𝐾)‘𝑊) = ((EDRing‘𝐾)‘𝑊) |
| 34 | 2, 33, 5, 6 | dvhsca 41084 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 = ((EDRing‘𝐾)‘𝑊)) |
| 35 | 2, 33 | erngdv 40995 |
. . . . . . . . 9
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ((EDRing‘𝐾)‘𝑊) ∈ DivRing) |
| 36 | 34, 35 | eqeltrd 2841 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ DivRing) |
| 37 | | drnggrp 20739 |
. . . . . . . 8
⊢ (𝐷 ∈ DivRing → 𝐷 ∈ Grp) |
| 38 | 36, 37 | syl 17 |
. . . . . . 7
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝐷 ∈ Grp) |
| 39 | 38 | adantr 480 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((2nd ‘𝐹) ∈ 𝐸 ∧ (2nd ‘𝐺) ∈ 𝐸 ∧ (2nd ‘𝐼) ∈ 𝐸)) → 𝐷 ∈ Grp) |
| 40 | | simpr1 1195 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((2nd ‘𝐹) ∈ 𝐸 ∧ (2nd ‘𝐺) ∈ 𝐸 ∧ (2nd ‘𝐼) ∈ 𝐸)) → (2nd ‘𝐹) ∈ 𝐸) |
| 41 | | eqid 2737 |
. . . . . . . . 9
⊢
(Base‘𝐷) =
(Base‘𝐷) |
| 42 | 2, 4, 5, 6, 41 | dvhbase 41085 |
. . . . . . . 8
⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (Base‘𝐷) = 𝐸) |
| 43 | 42 | adantr 480 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((2nd ‘𝐹) ∈ 𝐸 ∧ (2nd ‘𝐺) ∈ 𝐸 ∧ (2nd ‘𝐼) ∈ 𝐸)) → (Base‘𝐷) = 𝐸) |
| 44 | 40, 43 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((2nd ‘𝐹) ∈ 𝐸 ∧ (2nd ‘𝐺) ∈ 𝐸 ∧ (2nd ‘𝐼) ∈ 𝐸)) → (2nd ‘𝐹) ∈ (Base‘𝐷)) |
| 45 | | simpr2 1196 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((2nd ‘𝐹) ∈ 𝐸 ∧ (2nd ‘𝐺) ∈ 𝐸 ∧ (2nd ‘𝐼) ∈ 𝐸)) → (2nd ‘𝐺) ∈ 𝐸) |
| 46 | 45, 43 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((2nd ‘𝐹) ∈ 𝐸 ∧ (2nd ‘𝐺) ∈ 𝐸 ∧ (2nd ‘𝐼) ∈ 𝐸)) → (2nd ‘𝐺) ∈ (Base‘𝐷)) |
| 47 | | simpr3 1197 |
. . . . . . 7
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((2nd ‘𝐹) ∈ 𝐸 ∧ (2nd ‘𝐺) ∈ 𝐸 ∧ (2nd ‘𝐼) ∈ 𝐸)) → (2nd ‘𝐼) ∈ 𝐸) |
| 48 | 47, 43 | eleqtrrd 2844 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((2nd ‘𝐹) ∈ 𝐸 ∧ (2nd ‘𝐺) ∈ 𝐸 ∧ (2nd ‘𝐼) ∈ 𝐸)) → (2nd ‘𝐼) ∈ (Base‘𝐷)) |
| 49 | 41, 8 | grpass 18960 |
. . . . . 6
⊢ ((𝐷 ∈ Grp ∧
((2nd ‘𝐹)
∈ (Base‘𝐷) ∧
(2nd ‘𝐺)
∈ (Base‘𝐷) ∧
(2nd ‘𝐼)
∈ (Base‘𝐷)))
→ (((2nd ‘𝐹) ⨣ (2nd
‘𝐺)) ⨣
(2nd ‘𝐼))
= ((2nd ‘𝐹) ⨣ ((2nd
‘𝐺) ⨣
(2nd ‘𝐼)))) |
| 50 | 39, 44, 46, 48, 49 | syl13anc 1374 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((2nd ‘𝐹) ∈ 𝐸 ∧ (2nd ‘𝐺) ∈ 𝐸 ∧ (2nd ‘𝐼) ∈ 𝐸)) → (((2nd ‘𝐹) ⨣ (2nd
‘𝐺)) ⨣
(2nd ‘𝐼))
= ((2nd ‘𝐹) ⨣ ((2nd
‘𝐺) ⨣
(2nd ‘𝐼)))) |
| 51 | 32, 50 | sylan2 593 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (((2nd ‘𝐹) ⨣ (2nd
‘𝐺)) ⨣
(2nd ‘𝐼))
= ((2nd ‘𝐹) ⨣ ((2nd
‘𝐺) ⨣
(2nd ‘𝐼)))) |
| 52 | 10 | fveq2d 6910 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝐹 + 𝐺)) = (2nd
‘〈((1st ‘𝐹) ∘ (1st ‘𝐺)), ((2nd
‘𝐹) ⨣
(2nd ‘𝐺))〉)) |
| 53 | 14, 15 | op2nd 8023 |
. . . . . 6
⊢
(2nd ‘〈((1st ‘𝐹) ∘ (1st ‘𝐺)), ((2nd
‘𝐹) ⨣
(2nd ‘𝐺))〉) = ((2nd ‘𝐹) ⨣ (2nd
‘𝐺)) |
| 54 | 52, 53 | eqtrdi 2793 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝐹 + 𝐺)) = ((2nd ‘𝐹) ⨣ (2nd
‘𝐺))) |
| 55 | 54 | oveq1d 7446 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((2nd ‘(𝐹 + 𝐺)) ⨣ (2nd
‘𝐼)) =
(((2nd ‘𝐹)
⨣
(2nd ‘𝐺))
⨣
(2nd ‘𝐼))) |
| 56 | 20 | fveq2d 6910 |
. . . . . 6
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝐺 + 𝐼)) = (2nd
‘〈((1st ‘𝐺) ∘ (1st ‘𝐼)), ((2nd
‘𝐺) ⨣
(2nd ‘𝐼))〉)) |
| 57 | 23, 24 | op2nd 8023 |
. . . . . 6
⊢
(2nd ‘〈((1st ‘𝐺) ∘ (1st ‘𝐼)), ((2nd
‘𝐺) ⨣
(2nd ‘𝐼))〉) = ((2nd ‘𝐺) ⨣ (2nd
‘𝐼)) |
| 58 | 56, 57 | eqtrdi 2793 |
. . . . 5
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (2nd ‘(𝐺 + 𝐼)) = ((2nd ‘𝐺) ⨣ (2nd
‘𝐼))) |
| 59 | 58 | oveq2d 7447 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((2nd ‘𝐹) ⨣ (2nd
‘(𝐺 + 𝐼))) = ((2nd
‘𝐹) ⨣
((2nd ‘𝐺)
⨣
(2nd ‘𝐼)))) |
| 60 | 51, 55, 59 | 3eqtr4d 2787 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((2nd ‘(𝐹 + 𝐺)) ⨣ (2nd
‘𝐼)) =
((2nd ‘𝐹)
⨣
(2nd ‘(𝐺
+ 𝐼)))) |
| 61 | 28, 60 | opeq12d 4881 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → 〈((1st
‘(𝐹 + 𝐺)) ∘ (1st
‘𝐼)),
((2nd ‘(𝐹
+ 𝐺)) ⨣ (2nd
‘𝐼))〉 =
〈((1st ‘𝐹) ∘ (1st ‘(𝐺 + 𝐼))), ((2nd ‘𝐹) ⨣ (2nd
‘(𝐺 + 𝐼)))〉) |
| 62 | | simpl 482 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻)) |
| 63 | 2, 3, 4, 5, 6, 8, 7 | dvhvaddcl 41097 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) ∈ (𝑇 × 𝐸)) |
| 64 | 63 | 3adantr3 1172 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (𝐹 + 𝐺) ∈ (𝑇 × 𝐸)) |
| 65 | | simpr3 1197 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → 𝐼 ∈ (𝑇 × 𝐸)) |
| 66 | 2, 3, 4, 5, 6, 7, 8 | dvhvadd 41094 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝐹 + 𝐺) ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((𝐹 + 𝐺) + 𝐼) = 〈((1st ‘(𝐹 + 𝐺)) ∘ (1st ‘𝐼)), ((2nd
‘(𝐹 + 𝐺)) ⨣ (2nd
‘𝐼))〉) |
| 67 | 62, 64, 65, 66 | syl12anc 837 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((𝐹 + 𝐺) + 𝐼) = 〈((1st ‘(𝐹 + 𝐺)) ∘ (1st ‘𝐼)), ((2nd
‘(𝐹 + 𝐺)) ⨣ (2nd
‘𝐼))〉) |
| 68 | | simpr1 1195 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → 𝐹 ∈ (𝑇 × 𝐸)) |
| 69 | 2, 3, 4, 5, 6, 8, 7 | dvhvaddcl 41097 |
. . . 4
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (𝐺 + 𝐼) ∈ (𝑇 × 𝐸)) |
| 70 | 69 | 3adantr1 1170 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (𝐺 + 𝐼) ∈ (𝑇 × 𝐸)) |
| 71 | 2, 3, 4, 5, 6, 7, 8 | dvhvadd 41094 |
. . 3
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ (𝐺 + 𝐼) ∈ (𝑇 × 𝐸))) → (𝐹 + (𝐺 + 𝐼)) = 〈((1st ‘𝐹) ∘ (1st
‘(𝐺 + 𝐼))), ((2nd
‘𝐹) ⨣
(2nd ‘(𝐺
+ 𝐼)))〉) |
| 72 | 62, 68, 70, 71 | syl12anc 837 |
. 2
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → (𝐹 + (𝐺 + 𝐼)) = 〈((1st ‘𝐹) ∘ (1st
‘(𝐺 + 𝐼))), ((2nd
‘𝐹) ⨣
(2nd ‘(𝐺
+ 𝐼)))〉) |
| 73 | 61, 67, 72 | 3eqtr4d 2787 |
1
⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝐹 ∈ (𝑇 × 𝐸) ∧ 𝐺 ∈ (𝑇 × 𝐸) ∧ 𝐼 ∈ (𝑇 × 𝐸))) → ((𝐹 + 𝐺) + 𝐼) = (𝐹 + (𝐺 + 𝐼))) |