Step | Hyp | Ref
| Expression |
1 | | coass 6218 |
. . . 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 39558 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (πΉ + πΊ) = β¨((1st βπΉ) β (1st
βπΊ)),
((2nd βπΉ)
⨣
(2nd βπΊ))β©) |
10 | 9 | 3adantr3 1172 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (πΉ + πΊ) = β¨((1st βπΉ) β (1st
βπΊ)),
((2nd βπΉ)
⨣
(2nd βπΊ))β©) |
11 | 10 | fveq2d 6847 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (1st β(πΉ + πΊ)) = (1st
ββ¨((1st βπΉ) β (1st βπΊ)), ((2nd
βπΉ) ⨣
(2nd βπΊ))β©)) |
12 | | fvex 6856 |
. . . . . . . 8
β’
(1st βπΉ) β V |
13 | | fvex 6856 |
. . . . . . . 8
β’
(1st βπΊ) β V |
14 | 12, 13 | coex 7868 |
. . . . . . 7
β’
((1st βπΉ) β (1st βπΊ)) β V |
15 | | ovex 7391 |
. . . . . . 7
β’
((2nd βπΉ) ⨣ (2nd
βπΊ)) β
V |
16 | 14, 15 | op1st 7930 |
. . . . . 6
β’
(1st ββ¨((1st βπΉ) β (1st βπΊ)), ((2nd
βπΉ) ⨣
(2nd βπΊ))β©) = ((1st βπΉ) β (1st
βπΊ)) |
17 | 11, 16 | eqtrdi 2793 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (1st β(πΉ + πΊ)) = ((1st βπΉ) β (1st
βπΊ))) |
18 | 17 | coeq1d 5818 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β ((1st β(πΉ + πΊ)) β (1st βπΌ)) = (((1st
βπΉ) β
(1st βπΊ))
β (1st βπΌ))) |
19 | 2, 3, 4, 5, 6, 7, 8 | dvhvadd 39558 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (πΊ + πΌ) = β¨((1st βπΊ) β (1st
βπΌ)),
((2nd βπΊ)
⨣
(2nd βπΌ))β©) |
20 | 19 | 3adantr1 1170 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (πΊ + πΌ) = β¨((1st βπΊ) β (1st
βπΌ)),
((2nd βπΊ)
⨣
(2nd βπΌ))β©) |
21 | 20 | fveq2d 6847 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (1st β(πΊ + πΌ)) = (1st
ββ¨((1st βπΊ) β (1st βπΌ)), ((2nd
βπΊ) ⨣
(2nd βπΌ))β©)) |
22 | | fvex 6856 |
. . . . . . . 8
β’
(1st βπΌ) β V |
23 | 13, 22 | coex 7868 |
. . . . . . 7
β’
((1st βπΊ) β (1st βπΌ)) β V |
24 | | ovex 7391 |
. . . . . . 7
β’
((2nd βπΊ) ⨣ (2nd
βπΌ)) β
V |
25 | 23, 24 | op1st 7930 |
. . . . . 6
β’
(1st ββ¨((1st βπΊ) β (1st βπΌ)), ((2nd
βπΊ) ⨣
(2nd βπΌ))β©) = ((1st βπΊ) β (1st
βπΌ)) |
26 | 21, 25 | eqtrdi 2793 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (1st β(πΊ + πΌ)) = ((1st βπΊ) β (1st
βπΌ))) |
27 | 26 | coeq2d 5819 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β ((1st βπΉ) β (1st
β(πΊ + πΌ))) = ((1st
βπΉ) β
((1st βπΊ)
β (1st βπΌ)))) |
28 | 1, 18, 27 | 3eqtr4a 2803 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β ((1st β(πΉ + πΊ)) β (1st βπΌ)) = ((1st
βπΉ) β
(1st β(πΊ
+ πΌ)))) |
29 | | xp2nd 7955 |
. . . . . 6
β’ (πΉ β (π Γ πΈ) β (2nd βπΉ) β πΈ) |
30 | | xp2nd 7955 |
. . . . . 6
β’ (πΊ β (π Γ πΈ) β (2nd βπΊ) β πΈ) |
31 | | xp2nd 7955 |
. . . . . 6
β’ (πΌ β (π Γ πΈ) β (2nd βπΌ) β πΈ) |
32 | 29, 30, 31 | 3anim123i 1152 |
. . . . 5
β’ ((πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ)) β ((2nd βπΉ) β πΈ β§ (2nd βπΊ) β πΈ β§ (2nd βπΌ) β πΈ)) |
33 | | eqid 2737 |
. . . . . . . . . 10
β’
((EDRingβπΎ)βπ) = ((EDRingβπΎ)βπ) |
34 | 2, 33, 5, 6 | dvhsca 39548 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β π· = ((EDRingβπΎ)βπ)) |
35 | 2, 33 | erngdv 39459 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β ((EDRingβπΎ)βπ) β DivRing) |
36 | 34, 35 | eqeltrd 2838 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β π· β DivRing) |
37 | | drnggrp 20196 |
. . . . . . . 8
β’ (π· β DivRing β π· β Grp) |
38 | 36, 37 | syl 17 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β π· β Grp) |
39 | 38 | adantr 482 |
. . . . . 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 39549 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (Baseβπ·) = πΈ) |
43 | 42 | adantr 482 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ((2nd βπΉ) β πΈ β§ (2nd βπΊ) β πΈ β§ (2nd βπΌ) β πΈ)) β (Baseβπ·) = πΈ) |
44 | 40, 43 | eleqtrrd 2841 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((2nd βπΉ) β πΈ β§ (2nd βπΊ) β πΈ β§ (2nd βπΌ) β πΈ)) β (2nd βπΉ) β (Baseβπ·)) |
45 | | simpr2 1196 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ((2nd βπΉ) β πΈ β§ (2nd βπΊ) β πΈ β§ (2nd βπΌ) β πΈ)) β (2nd βπΊ) β πΈ) |
46 | 45, 43 | eleqtrrd 2841 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((2nd βπΉ) β πΈ β§ (2nd βπΊ) β πΈ β§ (2nd βπΌ) β πΈ)) β (2nd βπΊ) β (Baseβπ·)) |
47 | | simpr3 1197 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ ((2nd βπΉ) β πΈ β§ (2nd βπΊ) β πΈ β§ (2nd βπΌ) β πΈ)) β (2nd βπΌ) β πΈ) |
48 | 47, 43 | eleqtrrd 2841 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((2nd βπΉ) β πΈ β§ (2nd βπΊ) β πΈ β§ (2nd βπΌ) β πΈ)) β (2nd βπΌ) β (Baseβπ·)) |
49 | 41, 8 | grpass 18758 |
. . . . . 6
β’ ((π· β Grp β§
((2nd βπΉ)
β (Baseβπ·) β§
(2nd βπΊ)
β (Baseβπ·) β§
(2nd βπΌ)
β (Baseβπ·)))
β (((2nd βπΉ) ⨣ (2nd
βπΊ)) ⨣
(2nd βπΌ))
= ((2nd βπΉ) ⨣ ((2nd
βπΊ) ⨣
(2nd βπΌ)))) |
50 | 39, 44, 46, 48, 49 | syl13anc 1373 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((2nd βπΉ) β πΈ β§ (2nd βπΊ) β πΈ β§ (2nd βπΌ) β πΈ)) β (((2nd βπΉ) ⨣ (2nd
βπΊ)) ⨣
(2nd βπΌ))
= ((2nd βπΉ) ⨣ ((2nd
βπΊ) ⨣
(2nd βπΌ)))) |
51 | 32, 50 | sylan2 594 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (((2nd βπΉ) ⨣ (2nd
βπΊ)) ⨣
(2nd βπΌ))
= ((2nd βπΉ) ⨣ ((2nd
βπΊ) ⨣
(2nd βπΌ)))) |
52 | 10 | fveq2d 6847 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (2nd β(πΉ + πΊ)) = (2nd
ββ¨((1st βπΉ) β (1st βπΊ)), ((2nd
βπΉ) ⨣
(2nd βπΊ))β©)) |
53 | 14, 15 | op2nd 7931 |
. . . . . 6
β’
(2nd ββ¨((1st βπΉ) β (1st βπΊ)), ((2nd
βπΉ) ⨣
(2nd βπΊ))β©) = ((2nd βπΉ) ⨣ (2nd
βπΊ)) |
54 | 52, 53 | eqtrdi 2793 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (2nd β(πΉ + πΊ)) = ((2nd βπΉ) ⨣ (2nd
βπΊ))) |
55 | 54 | oveq1d 7373 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β ((2nd β(πΉ + πΊ)) ⨣ (2nd
βπΌ)) =
(((2nd βπΉ)
⨣
(2nd βπΊ))
⨣
(2nd βπΌ))) |
56 | 20 | fveq2d 6847 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (2nd β(πΊ + πΌ)) = (2nd
ββ¨((1st βπΊ) β (1st βπΌ)), ((2nd
βπΊ) ⨣
(2nd βπΌ))β©)) |
57 | 23, 24 | op2nd 7931 |
. . . . . 6
β’
(2nd ββ¨((1st βπΊ) β (1st βπΌ)), ((2nd
βπΊ) ⨣
(2nd βπΌ))β©) = ((2nd βπΊ) ⨣ (2nd
βπΌ)) |
58 | 56, 57 | eqtrdi 2793 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (2nd β(πΊ + πΌ)) = ((2nd βπΊ) ⨣ (2nd
βπΌ))) |
59 | 58 | oveq2d 7374 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β ((2nd βπΉ) ⨣ (2nd
β(πΊ + πΌ))) = ((2nd
βπΉ) ⨣
((2nd βπΊ)
⨣
(2nd βπΌ)))) |
60 | 51, 55, 59 | 3eqtr4d 2787 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β ((2nd β(πΉ + πΊ)) ⨣ (2nd
βπΌ)) =
((2nd βπΉ)
⨣
(2nd β(πΊ
+ πΌ)))) |
61 | 28, 60 | opeq12d 4839 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β β¨((1st
β(πΉ + πΊ)) β (1st
βπΌ)),
((2nd β(πΉ
+ πΊ)) ⨣ (2nd
βπΌ))β© =
β¨((1st βπΉ) β (1st β(πΊ + πΌ))), ((2nd βπΉ) ⨣ (2nd
β(πΊ + πΌ)))β©) |
62 | | simpl 484 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (πΎ β HL β§ π β π»)) |
63 | 2, 3, 4, 5, 6, 8, 7 | dvhvaddcl 39561 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (πΉ + πΊ) β (π Γ πΈ)) |
64 | 63 | 3adantr3 1172 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (πΉ + πΊ) β (π Γ πΈ)) |
65 | | simpr3 1197 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β πΌ β (π Γ πΈ)) |
66 | 2, 3, 4, 5, 6, 7, 8 | dvhvadd 39558 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((πΉ + πΊ) β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β ((πΉ + πΊ) + πΌ) = β¨((1st β(πΉ + πΊ)) β (1st βπΌ)), ((2nd
β(πΉ + πΊ)) ⨣ (2nd
βπΌ))β©) |
67 | 62, 64, 65, 66 | syl12anc 836 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β ((πΉ + πΊ) + πΌ) = β¨((1st β(πΉ + πΊ)) β (1st βπΌ)), ((2nd
β(πΉ + πΊ)) ⨣ (2nd
βπΌ))β©) |
68 | | simpr1 1195 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β πΉ β (π Γ πΈ)) |
69 | 2, 3, 4, 5, 6, 8, 7 | dvhvaddcl 39561 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (πΊ + πΌ) β (π Γ πΈ)) |
70 | 69 | 3adantr1 1170 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (πΊ + πΌ) β (π Γ πΈ)) |
71 | 2, 3, 4, 5, 6, 7, 8 | dvhvadd 39558 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ (πΊ + πΌ) β (π Γ πΈ))) β (πΉ + (πΊ + πΌ)) = β¨((1st βπΉ) β (1st
β(πΊ + πΌ))), ((2nd
βπΉ) ⨣
(2nd β(πΊ
+ πΌ)))β©) |
72 | 62, 68, 70, 71 | syl12anc 836 |
. 2
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β (πΉ + (πΊ + πΌ)) = β¨((1st βπΉ) β (1st
β(πΊ + πΌ))), ((2nd
βπΉ) ⨣
(2nd β(πΊ
+ πΌ)))β©) |
73 | 61, 67, 72 | 3eqtr4d 2787 |
1
β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β ((πΉ + πΊ) + πΌ) = (πΉ + (πΊ + πΌ))) |