Step | Hyp | Ref
| Expression |
1 | | dvhgrp.h |
. . . . 5
β’ π» = (LHypβπΎ) |
2 | | dvhgrp.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
3 | | dvhgrp.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
4 | | dvhgrp.u |
. . . . 5
β’ π = ((DVecHβπΎ)βπ) |
5 | | eqid 2738 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
6 | 1, 2, 3, 4, 5 | dvhvbase 39446 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (Baseβπ) = (π Γ πΈ)) |
7 | 6 | eqcomd 2744 |
. . 3
β’ ((πΎ β HL β§ π β π») β (π Γ πΈ) = (Baseβπ)) |
8 | | dvhgrp.a |
. . . 4
β’ + =
(+gβπ) |
9 | 8 | a1i 11 |
. . 3
β’ ((πΎ β HL β§ π β π») β + =
(+gβπ)) |
10 | | dvhgrp.d |
. . . 4
β’ π· = (Scalarβπ) |
11 | 10 | a1i 11 |
. . 3
β’ ((πΎ β HL β§ π β π») β π· = (Scalarβπ)) |
12 | | dvhlvec.s |
. . . 4
β’ Β· = (
Β·π βπ) |
13 | 12 | a1i 11 |
. . 3
β’ ((πΎ β HL β§ π β π») β Β· = (
Β·π βπ)) |
14 | | eqid 2738 |
. . . . 5
β’
(Baseβπ·) =
(Baseβπ·) |
15 | 1, 3, 4, 10, 14 | dvhbase 39442 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (Baseβπ·) = πΈ) |
16 | 15 | eqcomd 2744 |
. . 3
β’ ((πΎ β HL β§ π β π») β πΈ = (Baseβπ·)) |
17 | | dvhgrp.p |
. . . 4
⒠⨣ =
(+gβπ·) |
18 | 17 | a1i 11 |
. . 3
β’ ((πΎ β HL β§ π β π») β ⨣ =
(+gβπ·)) |
19 | | dvhlvec.m |
. . . 4
β’ Γ =
(.rβπ·) |
20 | 19 | a1i 11 |
. . 3
β’ ((πΎ β HL β§ π β π») β Γ =
(.rβπ·)) |
21 | | eqid 2738 |
. . . . . 6
β’
((EDRingβπΎ)βπ) = ((EDRingβπΎ)βπ) |
22 | 1, 21, 4, 10 | dvhsca 39441 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β π· = ((EDRingβπΎ)βπ)) |
23 | 22 | fveq2d 6842 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (1rβπ·) =
(1rβ((EDRingβπΎ)βπ))) |
24 | | eqid 2738 |
. . . . 5
β’
(1rβ((EDRingβπΎ)βπ)) =
(1rβ((EDRingβπΎ)βπ)) |
25 | 1, 2, 21, 24 | erng1r 39354 |
. . . 4
β’ ((πΎ β HL β§ π β π») β
(1rβ((EDRingβπΎ)βπ)) = ( I βΎ π)) |
26 | 23, 25 | eqtr2d 2779 |
. . 3
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) = (1rβπ·)) |
27 | 1, 21 | erngdv 39352 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β ((EDRingβπΎ)βπ) β DivRing) |
28 | 22, 27 | eqeltrd 2839 |
. . . 4
β’ ((πΎ β HL β§ π β π») β π· β DivRing) |
29 | | drngring 20116 |
. . . 4
β’ (π· β DivRing β π· β Ring) |
30 | 28, 29 | syl 17 |
. . 3
β’ ((πΎ β HL β§ π β π») β π· β Ring) |
31 | | dvhgrp.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
32 | | dvhgrp.o |
. . . 4
β’ 0 =
(0gβπ·) |
33 | | dvhgrp.i |
. . . 4
β’ πΌ = (invgβπ·) |
34 | 31, 1, 2, 3, 4, 10,
17, 8, 32, 33 | dvhgrp 39466 |
. . 3
β’ ((πΎ β HL β§ π β π») β π β Grp) |
35 | 1, 2, 3, 4, 12 | dvhvscacl 39462 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ))) β (π Β· π‘) β (π Γ πΈ)) |
36 | 35 | 3impb 1116 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β (π Γ πΈ)) β (π Β· π‘) β (π Γ πΈ)) |
37 | | simpl 484 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (πΎ β HL β§ π β π»)) |
38 | | simpr1 1195 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β π β πΈ) |
39 | | simpr2 1196 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β π‘ β (π Γ πΈ)) |
40 | | xp1st 7944 |
. . . . . . . 8
β’ (π‘ β (π Γ πΈ) β (1st βπ‘) β π) |
41 | 39, 40 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (1st βπ‘) β π) |
42 | | simpr3 1197 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β π β (π Γ πΈ)) |
43 | | xp1st 7944 |
. . . . . . . 8
β’ (π β (π Γ πΈ) β (1st βπ) β π) |
44 | 42, 43 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (1st βπ) β π) |
45 | 1, 2, 3 | tendospdi1 39379 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ (1st βπ‘) β π β§ (1st βπ) β π)) β (π β((1st βπ‘) β (1st
βπ))) = ((π β(1st
βπ‘)) β (π β(1st
βπ)))) |
46 | 37, 38, 41, 44, 45 | syl13anc 1373 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π β((1st βπ‘) β (1st
βπ))) = ((π β(1st
βπ‘)) β (π β(1st
βπ)))) |
47 | 1, 2, 3, 4, 10, 8,
17 | dvhvadd 39451 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π‘ + π) = β¨((1st βπ‘) β (1st
βπ)),
((2nd βπ‘)
⨣
(2nd βπ))β©) |
48 | 47 | 3adantr1 1170 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π‘ + π) = β¨((1st βπ‘) β (1st
βπ)),
((2nd βπ‘)
⨣
(2nd βπ))β©) |
49 | 48 | fveq2d 6842 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (1st β(π‘ + π)) = (1st
ββ¨((1st βπ‘) β (1st βπ)), ((2nd
βπ‘) ⨣
(2nd βπ))β©)) |
50 | | fvex 6851 |
. . . . . . . . . 10
β’
(1st βπ‘) β V |
51 | | fvex 6851 |
. . . . . . . . . 10
β’
(1st βπ) β V |
52 | 50, 51 | coex 7858 |
. . . . . . . . 9
β’
((1st βπ‘) β (1st βπ)) β V |
53 | | ovex 7383 |
. . . . . . . . 9
β’
((2nd βπ‘) ⨣ (2nd
βπ)) β
V |
54 | 52, 53 | op1st 7920 |
. . . . . . . 8
β’
(1st ββ¨((1st βπ‘) β (1st βπ)), ((2nd
βπ‘) ⨣
(2nd βπ))β©) = ((1st βπ‘) β (1st
βπ)) |
55 | 49, 54 | eqtrdi 2794 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (1st β(π‘ + π)) = ((1st βπ‘) β (1st
βπ))) |
56 | 55 | fveq2d 6842 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π β(1st β(π‘ + π))) = (π β((1st βπ‘) β (1st
βπ)))) |
57 | 1, 2, 3, 4, 12 | dvhvsca 39460 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ))) β (π Β· π‘) = β¨(π β(1st βπ‘)), (π β (2nd βπ‘))β©) |
58 | 57 | 3adantr3 1172 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π Β· π‘) = β¨(π β(1st βπ‘)), (π β (2nd βπ‘))β©) |
59 | 58 | fveq2d 6842 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (1st β(π Β· π‘)) = (1st ββ¨(π β(1st
βπ‘)), (π β (2nd
βπ‘))β©)) |
60 | | fvex 6851 |
. . . . . . . . 9
β’ (π β(1st
βπ‘)) β
V |
61 | | vex 3448 |
. . . . . . . . . 10
β’ π β V |
62 | | fvex 6851 |
. . . . . . . . . 10
β’
(2nd βπ‘) β V |
63 | 61, 62 | coex 7858 |
. . . . . . . . 9
β’ (π β (2nd
βπ‘)) β
V |
64 | 60, 63 | op1st 7920 |
. . . . . . . 8
β’
(1st ββ¨(π β(1st βπ‘)), (π β (2nd βπ‘))β©) = (π β(1st βπ‘)) |
65 | 59, 64 | eqtrdi 2794 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (1st β(π Β· π‘)) = (π β(1st βπ‘))) |
66 | 1, 2, 3, 4, 12 | dvhvsca 39460 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β (π Γ πΈ))) β (π Β· π) = β¨(π β(1st βπ)), (π β (2nd βπ))β©) |
67 | 66 | 3adantr2 1171 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π Β· π) = β¨(π β(1st βπ)), (π β (2nd βπ))β©) |
68 | 67 | fveq2d 6842 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (1st β(π Β· π)) = (1st ββ¨(π β(1st
βπ)), (π β (2nd
βπ))β©)) |
69 | | fvex 6851 |
. . . . . . . . 9
β’ (π β(1st
βπ)) β
V |
70 | | fvex 6851 |
. . . . . . . . . 10
β’
(2nd βπ) β V |
71 | 61, 70 | coex 7858 |
. . . . . . . . 9
β’ (π β (2nd
βπ)) β
V |
72 | 69, 71 | op1st 7920 |
. . . . . . . 8
β’
(1st ββ¨(π β(1st βπ)), (π β (2nd βπ))β©) = (π β(1st βπ)) |
73 | 68, 72 | eqtrdi 2794 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (1st β(π Β· π)) = (π β(1st βπ))) |
74 | 65, 73 | coeq12d 5817 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β ((1st β(π Β· π‘)) β (1st β(π Β· π))) = ((π β(1st βπ‘)) β (π β(1st βπ)))) |
75 | 46, 56, 74 | 3eqtr4d 2788 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π β(1st β(π‘ + π))) = ((1st β(π Β· π‘)) β (1st β(π Β· π)))) |
76 | 30 | adantr 482 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β π· β Ring) |
77 | 16 | adantr 482 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β πΈ = (Baseβπ·)) |
78 | 38, 77 | eleqtrd 2841 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β π β (Baseβπ·)) |
79 | | xp2nd 7945 |
. . . . . . . . . 10
β’ (π‘ β (π Γ πΈ) β (2nd βπ‘) β πΈ) |
80 | 39, 79 | syl 17 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (2nd βπ‘) β πΈ) |
81 | 80, 77 | eleqtrd 2841 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (2nd βπ‘) β (Baseβπ·)) |
82 | | xp2nd 7945 |
. . . . . . . . . 10
β’ (π β (π Γ πΈ) β (2nd βπ) β πΈ) |
83 | 42, 82 | syl 17 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (2nd βπ) β πΈ) |
84 | 83, 77 | eleqtrd 2841 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (2nd βπ) β (Baseβπ·)) |
85 | 14, 17, 19 | ringdi 19912 |
. . . . . . . 8
β’ ((π· β Ring β§ (π β (Baseβπ·) β§ (2nd
βπ‘) β
(Baseβπ·) β§
(2nd βπ)
β (Baseβπ·)))
β (π Γ
((2nd βπ‘)
⨣
(2nd βπ)))
= ((π Γ (2nd
βπ‘)) ⨣ (π Γ (2nd
βπ)))) |
86 | 76, 78, 81, 84, 85 | syl13anc 1373 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π Γ ((2nd
βπ‘) ⨣
(2nd βπ)))
= ((π Γ (2nd
βπ‘)) ⨣ (π Γ (2nd
βπ)))) |
87 | 14, 17 | ringacl 19924 |
. . . . . . . . . 10
β’ ((π· β Ring β§
(2nd βπ‘)
β (Baseβπ·) β§
(2nd βπ)
β (Baseβπ·))
β ((2nd βπ‘) ⨣ (2nd
βπ)) β
(Baseβπ·)) |
88 | 76, 81, 84, 87 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β ((2nd βπ‘) ⨣ (2nd
βπ)) β
(Baseβπ·)) |
89 | 88, 77 | eleqtrrd 2842 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β ((2nd βπ‘) ⨣ (2nd
βπ)) β πΈ) |
90 | 1, 2, 3, 4, 10, 19 | dvhmulr 39445 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ ((2nd βπ‘) ⨣ (2nd
βπ)) β πΈ)) β (π Γ ((2nd
βπ‘) ⨣
(2nd βπ)))
= (π β
((2nd βπ‘)
⨣
(2nd βπ)))) |
91 | 37, 38, 89, 90 | syl12anc 836 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π Γ ((2nd
βπ‘) ⨣
(2nd βπ)))
= (π β
((2nd βπ‘)
⨣
(2nd βπ)))) |
92 | 1, 2, 3, 4, 10, 19 | dvhmulr 39445 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ (2nd βπ‘) β πΈ)) β (π Γ (2nd
βπ‘)) = (π β (2nd
βπ‘))) |
93 | 37, 38, 80, 92 | syl12anc 836 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π Γ (2nd
βπ‘)) = (π β (2nd
βπ‘))) |
94 | 1, 2, 3, 4, 10, 19 | dvhmulr 39445 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ (2nd βπ) β πΈ)) β (π Γ (2nd
βπ)) = (π β (2nd
βπ))) |
95 | 37, 38, 83, 94 | syl12anc 836 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π Γ (2nd
βπ)) = (π β (2nd
βπ))) |
96 | 93, 95 | oveq12d 7368 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β ((π Γ (2nd
βπ‘)) ⨣ (π Γ (2nd
βπ))) = ((π β (2nd
βπ‘)) ⨣ (π β (2nd
βπ)))) |
97 | 86, 91, 96 | 3eqtr3d 2786 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π β ((2nd βπ‘) ⨣ (2nd
βπ))) = ((π β (2nd
βπ‘)) ⨣ (π β (2nd
βπ)))) |
98 | 48 | fveq2d 6842 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (2nd β(π‘ + π)) = (2nd
ββ¨((1st βπ‘) β (1st βπ)), ((2nd
βπ‘) ⨣
(2nd βπ))β©)) |
99 | 52, 53 | op2nd 7921 |
. . . . . . . 8
β’
(2nd ββ¨((1st βπ‘) β (1st βπ)), ((2nd
βπ‘) ⨣
(2nd βπ))β©) = ((2nd βπ‘) ⨣ (2nd
βπ)) |
100 | 98, 99 | eqtrdi 2794 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (2nd β(π‘ + π)) = ((2nd βπ‘) ⨣ (2nd
βπ))) |
101 | 100 | coeq2d 5815 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π β (2nd β(π‘ + π))) = (π β ((2nd βπ‘) ⨣ (2nd
βπ)))) |
102 | 58 | fveq2d 6842 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (2nd β(π Β· π‘)) = (2nd ββ¨(π β(1st
βπ‘)), (π β (2nd
βπ‘))β©)) |
103 | 60, 63 | op2nd 7921 |
. . . . . . . 8
β’
(2nd ββ¨(π β(1st βπ‘)), (π β (2nd βπ‘))β©) = (π β (2nd βπ‘)) |
104 | 102, 103 | eqtrdi 2794 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (2nd β(π Β· π‘)) = (π β (2nd βπ‘))) |
105 | 67 | fveq2d 6842 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (2nd β(π Β· π)) = (2nd ββ¨(π β(1st
βπ)), (π β (2nd
βπ))β©)) |
106 | 69, 71 | op2nd 7921 |
. . . . . . . 8
β’
(2nd ββ¨(π β(1st βπ)), (π β (2nd βπ))β©) = (π β (2nd βπ)) |
107 | 105, 106 | eqtrdi 2794 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (2nd β(π Β· π)) = (π β (2nd βπ))) |
108 | 104, 107 | oveq12d 7368 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β ((2nd β(π Β· π‘)) ⨣ (2nd
β(π Β· π))) = ((π β (2nd βπ‘)) ⨣ (π β (2nd βπ)))) |
109 | 97, 101, 108 | 3eqtr4d 2788 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π β (2nd β(π‘ + π))) = ((2nd β(π Β· π‘)) ⨣ (2nd
β(π Β· π)))) |
110 | 75, 109 | opeq12d 4837 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β β¨(π β(1st β(π‘ + π))), (π β (2nd β(π‘ + π)))β© = β¨((1st
β(π Β· π‘)) β (1st
β(π Β· π))), ((2nd
β(π Β· π‘)) ⨣ (2nd
β(π Β· π)))β©) |
111 | 1, 2, 3, 4, 10, 17, 8 | dvhvaddcl 39454 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π‘ + π) β (π Γ πΈ)) |
112 | 111 | 3adantr1 1170 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π‘ + π) β (π Γ πΈ)) |
113 | 1, 2, 3, 4, 12 | dvhvsca 39460 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ (π‘ + π) β (π Γ πΈ))) β (π Β· (π‘ + π)) = β¨(π β(1st β(π‘ + π))), (π β (2nd β(π‘ + π)))β©) |
114 | 37, 38, 112, 113 | syl12anc 836 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π Β· (π‘ + π)) = β¨(π β(1st β(π‘ + π))), (π β (2nd β(π‘ + π)))β©) |
115 | 35 | 3adantr3 1172 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π Β· π‘) β (π Γ πΈ)) |
116 | 1, 2, 3, 4, 12 | dvhvscacl 39462 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β (π Γ πΈ))) β (π Β· π) β (π Γ πΈ)) |
117 | 116 | 3adantr2 1171 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π Β· π) β (π Γ πΈ)) |
118 | 1, 2, 3, 4, 10, 8,
17 | dvhvadd 39451 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π Β· π‘) β (π Γ πΈ) β§ (π Β· π) β (π Γ πΈ))) β ((π Β· π‘) + (π Β· π)) = β¨((1st β(π Β· π‘)) β (1st β(π Β· π))), ((2nd β(π Β· π‘)) ⨣ (2nd
β(π Β· π)))β©) |
119 | 37, 115, 117, 118 | syl12anc 836 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β ((π Β· π‘) + (π Β· π)) = β¨((1st β(π Β· π‘)) β (1st β(π Β· π))), ((2nd β(π Β· π‘)) ⨣ (2nd
β(π Β· π)))β©) |
120 | 110, 114,
119 | 3eqtr4d 2788 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β (π Γ πΈ) β§ π β (π Γ πΈ))) β (π Β· (π‘ + π)) = ((π Β· π‘) + (π Β· π))) |
121 | | simpl 484 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (πΎ β HL β§ π β π»)) |
122 | | simpr1 1195 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β π β πΈ) |
123 | | simpr2 1196 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β π‘ β πΈ) |
124 | | simpr3 1197 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β π β (π Γ πΈ)) |
125 | 124, 43 | syl 17 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (1st βπ) β π) |
126 | | eqid 2738 |
. . . . . . . 8
β’
(+gβ((EDRingβπΎ)βπ)) =
(+gβ((EDRingβπΎ)βπ)) |
127 | 1, 2, 3, 21, 126 | erngplus2 39163 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ (1st βπ) β π)) β ((π (+gβ((EDRingβπΎ)βπ))π‘)β(1st βπ)) = ((π β(1st βπ)) β (π‘β(1st βπ)))) |
128 | 121, 122,
123, 125, 127 | syl13anc 1373 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π (+gβ((EDRingβπΎ)βπ))π‘)β(1st βπ)) = ((π β(1st βπ)) β (π‘β(1st βπ)))) |
129 | 22 | fveq2d 6842 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π») β (+gβπ·) =
(+gβ((EDRingβπΎ)βπ))) |
130 | 17, 129 | eqtrid 2790 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β ⨣ =
(+gβ((EDRingβπΎ)βπ))) |
131 | 130 | oveqd 7367 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (π ⨣ π‘) = (π (+gβ((EDRingβπΎ)βπ))π‘)) |
132 | 131 | fveq1d 6840 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β ((π ⨣ π‘)β(1st βπ)) = ((π (+gβ((EDRingβπΎ)βπ))π‘)β(1st βπ))) |
133 | 132 | adantr 482 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π ⨣ π‘)β(1st βπ)) = ((π (+gβ((EDRingβπΎ)βπ))π‘)β(1st βπ))) |
134 | 66 | 3adantr2 1171 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π Β· π) = β¨(π β(1st βπ)), (π β (2nd βπ))β©) |
135 | 134 | fveq2d 6842 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (1st β(π Β· π)) = (1st ββ¨(π β(1st
βπ)), (π β (2nd
βπ))β©)) |
136 | 135, 72 | eqtrdi 2794 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (1st β(π Β· π)) = (π β(1st βπ))) |
137 | 1, 2, 3, 4, 12 | dvhvsca 39460 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (π‘ β πΈ β§ π β (π Γ πΈ))) β (π‘ Β· π) = β¨(π‘β(1st βπ)), (π‘ β (2nd βπ))β©) |
138 | 137 | 3adantr1 1170 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π‘ Β· π) = β¨(π‘β(1st βπ)), (π‘ β (2nd βπ))β©) |
139 | 138 | fveq2d 6842 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (1st β(π‘ Β· π)) = (1st ββ¨(π‘β(1st
βπ)), (π‘ β (2nd
βπ))β©)) |
140 | | fvex 6851 |
. . . . . . . . 9
β’ (π‘β(1st
βπ)) β
V |
141 | | vex 3448 |
. . . . . . . . . 10
β’ π‘ β V |
142 | 141, 70 | coex 7858 |
. . . . . . . . 9
β’ (π‘ β (2nd
βπ)) β
V |
143 | 140, 142 | op1st 7920 |
. . . . . . . 8
β’
(1st ββ¨(π‘β(1st βπ)), (π‘ β (2nd βπ))β©) = (π‘β(1st βπ)) |
144 | 139, 143 | eqtrdi 2794 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (1st β(π‘ Β· π)) = (π‘β(1st βπ))) |
145 | 136, 144 | coeq12d 5817 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((1st β(π Β· π)) β (1st β(π‘ Β· π))) = ((π β(1st βπ)) β (π‘β(1st βπ)))) |
146 | 128, 133,
145 | 3eqtr4d 2788 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π ⨣ π‘)β(1st βπ)) = ((1st
β(π Β· π)) β (1st
β(π‘ Β· π)))) |
147 | 30 | adantr 482 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β π· β Ring) |
148 | 16 | adantr 482 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β πΈ = (Baseβπ·)) |
149 | 122, 148 | eleqtrd 2841 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β π β (Baseβπ·)) |
150 | 123, 148 | eleqtrd 2841 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β π‘ β (Baseβπ·)) |
151 | 124, 82 | syl 17 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (2nd βπ) β πΈ) |
152 | 151, 148 | eleqtrd 2841 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (2nd βπ) β (Baseβπ·)) |
153 | 14, 17, 19 | ringdir 19913 |
. . . . . . . 8
β’ ((π· β Ring β§ (π β (Baseβπ·) β§ π‘ β (Baseβπ·) β§ (2nd βπ) β (Baseβπ·))) β ((π ⨣ π‘) Γ (2nd
βπ)) = ((π Γ (2nd
βπ)) ⨣ (π‘ Γ (2nd
βπ)))) |
154 | 147, 149,
150, 152, 153 | syl13anc 1373 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π ⨣ π‘) Γ (2nd
βπ)) = ((π Γ (2nd
βπ)) ⨣ (π‘ Γ (2nd
βπ)))) |
155 | 14, 17 | ringacl 19924 |
. . . . . . . . . 10
β’ ((π· β Ring β§ π β (Baseβπ·) β§ π‘ β (Baseβπ·)) β (π ⨣ π‘) β (Baseβπ·)) |
156 | 147, 149,
150, 155 | syl3anc 1372 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π ⨣ π‘) β (Baseβπ·)) |
157 | 156, 148 | eleqtrrd 2842 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π ⨣ π‘) β πΈ) |
158 | 1, 2, 3, 4, 10, 19 | dvhmulr 39445 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ ((π ⨣ π‘) β πΈ β§ (2nd βπ) β πΈ)) β ((π ⨣ π‘) Γ (2nd
βπ)) = ((π ⨣ π‘) β (2nd βπ))) |
159 | 121, 157,
151, 158 | syl12anc 836 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π ⨣ π‘) Γ (2nd
βπ)) = ((π ⨣ π‘) β (2nd βπ))) |
160 | 121, 122,
151, 94 | syl12anc 836 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π Γ (2nd
βπ)) = (π β (2nd
βπ))) |
161 | 1, 2, 3, 4, 10, 19 | dvhmulr 39445 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ (π‘ β πΈ β§ (2nd βπ) β πΈ)) β (π‘ Γ (2nd
βπ)) = (π‘ β (2nd
βπ))) |
162 | 121, 123,
151, 161 | syl12anc 836 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π‘ Γ (2nd
βπ)) = (π‘ β (2nd
βπ))) |
163 | 160, 162 | oveq12d 7368 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π Γ (2nd
βπ)) ⨣ (π‘ Γ (2nd
βπ))) = ((π β (2nd
βπ)) ⨣ (π‘ β (2nd
βπ)))) |
164 | 154, 159,
163 | 3eqtr3d 2786 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π ⨣ π‘) β (2nd βπ)) = ((π β (2nd βπ)) ⨣ (π‘ β (2nd βπ)))) |
165 | 134 | fveq2d 6842 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (2nd β(π Β· π)) = (2nd ββ¨(π β(1st
βπ)), (π β (2nd
βπ))β©)) |
166 | 165, 106 | eqtrdi 2794 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (2nd β(π Β· π)) = (π β (2nd βπ))) |
167 | 138 | fveq2d 6842 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (2nd β(π‘ Β· π)) = (2nd ββ¨(π‘β(1st
βπ)), (π‘ β (2nd
βπ))β©)) |
168 | 140, 142 | op2nd 7921 |
. . . . . . . 8
β’
(2nd ββ¨(π‘β(1st βπ)), (π‘ β (2nd βπ))β©) = (π‘ β (2nd βπ)) |
169 | 167, 168 | eqtrdi 2794 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (2nd β(π‘ Β· π)) = (π‘ β (2nd βπ))) |
170 | 166, 169 | oveq12d 7368 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((2nd β(π Β· π)) ⨣ (2nd
β(π‘ Β· π))) = ((π β (2nd βπ)) ⨣ (π‘ β (2nd βπ)))) |
171 | 164, 170 | eqtr4d 2781 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π ⨣ π‘) β (2nd βπ)) = ((2nd
β(π Β· π)) ⨣ (2nd
β(π‘ Β· π)))) |
172 | 146, 171 | opeq12d 4837 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β β¨((π ⨣ π‘)β(1st βπ)), ((π ⨣ π‘) β (2nd βπ))β© =
β¨((1st β(π Β· π)) β (1st β(π‘ Β· π))), ((2nd β(π Β· π)) ⨣ (2nd
β(π‘ Β· π)))β©) |
173 | 1, 2, 3, 4, 12 | dvhvsca 39460 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π ⨣ π‘) β πΈ β§ π β (π Γ πΈ))) β ((π ⨣ π‘) Β· π) = β¨((π ⨣ π‘)β(1st βπ)), ((π ⨣ π‘) β (2nd βπ))β©) |
174 | 121, 157,
124, 173 | syl12anc 836 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π ⨣ π‘) Β· π) = β¨((π ⨣ π‘)β(1st βπ)), ((π ⨣ π‘) β (2nd βπ))β©) |
175 | 116 | 3adantr2 1171 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π Β· π) β (π Γ πΈ)) |
176 | 1, 2, 3, 4, 12 | dvhvscacl 39462 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π‘ β πΈ β§ π β (π Γ πΈ))) β (π‘ Β· π) β (π Γ πΈ)) |
177 | 176 | 3adantr1 1170 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π‘ Β· π) β (π Γ πΈ)) |
178 | 1, 2, 3, 4, 10, 8,
17 | dvhvadd 39451 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π Β· π) β (π Γ πΈ) β§ (π‘ Β· π) β (π Γ πΈ))) β ((π Β· π) + (π‘ Β· π)) = β¨((1st β(π Β· π)) β (1st β(π‘ Β· π))), ((2nd β(π Β· π)) ⨣ (2nd
β(π‘ Β· π)))β©) |
179 | 121, 175,
177, 178 | syl12anc 836 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π Β· π) + (π‘ Β· π)) = β¨((1st β(π Β· π)) β (1st β(π‘ Β· π))), ((2nd β(π Β· π)) ⨣ (2nd
β(π‘ Β· π)))β©) |
180 | 172, 174,
179 | 3eqtr4d 2788 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π ⨣ π‘) Β· π) = ((π Β· π) + (π‘ Β· π))) |
181 | 1, 2, 3 | tendocoval 39125 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ) β§ (1st βπ) β π) β ((π β π‘)β(1st βπ)) = (π β(π‘β(1st βπ)))) |
182 | 121, 122,
123, 125, 181 | syl121anc 1376 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π β π‘)β(1st βπ)) = (π β(π‘β(1st βπ)))) |
183 | | coass 6214 |
. . . . . . 7
β’ ((π β π‘) β (2nd βπ)) = (π β (π‘ β (2nd βπ))) |
184 | 183 | a1i 11 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π β π‘) β (2nd βπ)) = (π β (π‘ β (2nd βπ)))) |
185 | 182, 184 | opeq12d 4837 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β β¨((π β π‘)β(1st βπ)), ((π β π‘) β (2nd βπ))β© = β¨(π β(π‘β(1st βπ))), (π β (π‘ β (2nd βπ)))β©) |
186 | 1, 3 | tendococl 39131 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β πΈ) β (π β π‘) β πΈ) |
187 | 121, 122,
123, 186 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π β π‘) β πΈ) |
188 | 1, 2, 3, 4, 12 | dvhvsca 39460 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π‘) β πΈ β§ π β (π Γ πΈ))) β ((π β π‘) Β· π) = β¨((π β π‘)β(1st βπ)), ((π β π‘) β (2nd βπ))β©) |
189 | 121, 187,
124, 188 | syl12anc 836 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π β π‘) Β· π) = β¨((π β π‘)β(1st βπ)), ((π β π‘) β (2nd βπ))β©) |
190 | 1, 2, 3 | tendocl 39126 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π‘ β πΈ β§ (1st βπ) β π) β (π‘β(1st βπ)) β π) |
191 | 121, 123,
125, 190 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π‘β(1st βπ)) β π) |
192 | 1, 3 | tendococl 39131 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π‘ β πΈ β§ (2nd βπ) β πΈ) β (π‘ β (2nd βπ)) β πΈ) |
193 | 121, 123,
151, 192 | syl3anc 1372 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π‘ β (2nd βπ)) β πΈ) |
194 | 1, 2, 3, 4, 12 | dvhopvsca 39461 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ (π‘β(1st βπ)) β π β§ (π‘ β (2nd βπ)) β πΈ)) β (π Β· β¨(π‘β(1st
βπ)), (π‘ β (2nd
βπ))β©) =
β¨(π β(π‘β(1st
βπ))), (π β (π‘ β (2nd βπ)))β©) |
195 | 121, 122,
191, 193, 194 | syl13anc 1373 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π Β· β¨(π‘β(1st
βπ)), (π‘ β (2nd
βπ))β©) =
β¨(π β(π‘β(1st
βπ))), (π β (π‘ β (2nd βπ)))β©) |
196 | 185, 189,
195 | 3eqtr4d 2788 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π β π‘) Β· π) = (π Β· β¨(π‘β(1st
βπ)), (π‘ β (2nd
βπ))β©)) |
197 | 1, 2, 3, 4, 10, 19 | dvhmulr 39445 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ)) β (π Γ π‘) = (π β π‘)) |
198 | 197 | 3adantr3 1172 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π Γ π‘) = (π β π‘)) |
199 | 198 | oveq1d 7365 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π Γ π‘) Β· π) = ((π β π‘) Β· π)) |
200 | 138 | oveq2d 7366 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β (π Β· (π‘ Β· π)) = (π Β· β¨(π‘β(1st
βπ)), (π‘ β (2nd
βπ))β©)) |
201 | 196, 199,
200 | 3eqtr4d 2788 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β (π Γ πΈ))) β ((π Γ π‘) Β· π) = (π Β· (π‘ Β· π))) |
202 | | xp1st 7944 |
. . . . . . 7
β’ (π β (π Γ πΈ) β (1st βπ ) β π) |
203 | 202 | adantl 483 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (1st βπ ) β π) |
204 | | fvresi 7114 |
. . . . . 6
β’
((1st βπ ) β π β (( I βΎ π)β(1st βπ )) = (1st
βπ )) |
205 | 203, 204 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (( I βΎ π)β(1st βπ )) = (1st
βπ )) |
206 | | xp2nd 7945 |
. . . . . . 7
β’ (π β (π Γ πΈ) β (2nd βπ ) β πΈ) |
207 | 1, 2, 3 | tendof 39122 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (2nd βπ ) β πΈ) β (2nd βπ ):πβΆπ) |
208 | 206, 207 | sylan2 594 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (2nd βπ ):πβΆπ) |
209 | | fcoi2 6713 |
. . . . . 6
β’
((2nd βπ ):πβΆπ β (( I βΎ π) β (2nd βπ )) = (2nd
βπ )) |
210 | 208, 209 | syl 17 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (( I βΎ π) β (2nd βπ )) = (2nd
βπ )) |
211 | 205, 210 | opeq12d 4837 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β β¨(( I βΎ π)β(1st
βπ )), (( I βΎ
π) β (2nd
βπ ))β© =
β¨(1st βπ ), (2nd βπ )β©) |
212 | 1, 2, 3 | tendoidcl 39128 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β πΈ) |
213 | 212 | anim1i 616 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (( I βΎ π) β πΈ β§ π β (π Γ πΈ))) |
214 | 1, 2, 3, 4, 12 | dvhvsca 39460 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (( I βΎ π) β πΈ β§ π β (π Γ πΈ))) β (( I βΎ π) Β· π ) = β¨(( I βΎ π)β(1st βπ )), (( I βΎ π) β (2nd
βπ ))β©) |
215 | 213, 214 | syldan 592 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (( I βΎ π) Β· π ) = β¨(( I βΎ π)β(1st βπ )), (( I βΎ π) β (2nd
βπ ))β©) |
216 | | 1st2nd2 7951 |
. . . . 5
β’ (π β (π Γ πΈ) β π = β¨(1st βπ ), (2nd βπ )β©) |
217 | 216 | adantl 483 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β π = β¨(1st βπ ), (2nd βπ )β©) |
218 | 211, 215,
217 | 3eqtr4d 2788 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β (π Γ πΈ)) β (( I βΎ π) Β· π ) = π ) |
219 | 7, 9, 11, 13, 16, 18, 20, 26, 30, 34, 36, 120, 180, 201, 218 | islmodd 20252 |
. 2
β’ ((πΎ β HL β§ π β π») β π β LMod) |
220 | 10 | islvec 20489 |
. 2
β’ (π β LVec β (π β LMod β§ π· β
DivRing)) |
221 | 219, 28, 220 | sylanbrc 584 |
1
β’ ((πΎ β HL β§ π β π») β π β LVec) |