Step | Hyp | Ref
| Expression |
1 | | dvalvec.h |
. . . . 5
β’ π» = (LHypβπΎ) |
2 | | dvalveclem.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
3 | | dvalvec.v |
. . . . 5
β’ π = ((DVecAβπΎ)βπ) |
4 | | eqid 2737 |
. . . . 5
β’
(Baseβπ) =
(Baseβπ) |
5 | 1, 2, 3, 4 | dvavbase 39505 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (Baseβπ) = π) |
6 | 5 | eqcomd 2743 |
. . 3
β’ ((πΎ β HL β§ π β π») β π = (Baseβπ)) |
7 | | dvalveclem.a |
. . . 4
β’ + =
(+gβπ) |
8 | 7 | a1i 11 |
. . 3
β’ ((πΎ β HL β§ π β π») β + =
(+gβπ)) |
9 | | dvalveclem.d |
. . . 4
β’ π· = (Scalarβπ) |
10 | 9 | a1i 11 |
. . 3
β’ ((πΎ β HL β§ π β π») β π· = (Scalarβπ)) |
11 | | dvalveclem.s |
. . . 4
β’ Β· = (
Β·π βπ) |
12 | 11 | a1i 11 |
. . 3
β’ ((πΎ β HL β§ π β π») β Β· = (
Β·π βπ)) |
13 | | dvalveclem.e |
. . . . 5
β’ πΈ = ((TEndoβπΎ)βπ) |
14 | | eqid 2737 |
. . . . 5
β’
(Baseβπ·) =
(Baseβπ·) |
15 | 1, 13, 3, 9, 14 | dvabase 39499 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (Baseβπ·) = πΈ) |
16 | 15 | eqcomd 2743 |
. . 3
β’ ((πΎ β HL β§ π β π») β πΈ = (Baseβπ·)) |
17 | | dvalveclem.p |
. . . 4
⒠⨣ =
(+gβπ·) |
18 | 17 | a1i 11 |
. . 3
β’ ((πΎ β HL β§ π β π») β ⨣ =
(+gβπ·)) |
19 | | dvalveclem.m |
. . . 4
β’ Γ =
(.rβπ·) |
20 | 19 | a1i 11 |
. . 3
β’ ((πΎ β HL β§ π β π») β Γ =
(.rβπ·)) |
21 | 1, 2, 13 | tendoidcl 39261 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β πΈ) |
22 | 21, 16 | eleqtrd 2840 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β (Baseβπ·)) |
23 | | dvalveclem.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
24 | | eqid 2737 |
. . . . . . . 8
β’ (π β π β¦ ( I βΎ π΅)) = (π β π β¦ ( I βΎ π΅)) |
25 | 23, 1, 2, 13, 24 | tendo1ne0 39320 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β (π β π β¦ ( I βΎ π΅))) |
26 | | eqid 2737 |
. . . . . . . . . 10
β’
((EDRingβπΎ)βπ) = ((EDRingβπΎ)βπ) |
27 | 1, 26, 3, 9 | dvasca 39498 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β π») β π· = ((EDRingβπΎ)βπ)) |
28 | 27 | fveq2d 6851 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (0gβπ·) =
(0gβ((EDRingβπΎ)βπ))) |
29 | | eqid 2737 |
. . . . . . . . 9
β’
(0gβ((EDRingβπΎ)βπ)) =
(0gβ((EDRingβπΎ)βπ)) |
30 | 23, 1, 2, 26, 24, 29 | erng0g 39486 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β
(0gβ((EDRingβπΎ)βπ)) = (π β π β¦ ( I βΎ π΅))) |
31 | 28, 30 | eqtrd 2777 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β (0gβπ·) = (π β π β¦ ( I βΎ π΅))) |
32 | 25, 31 | neeqtrrd 3019 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β (0gβπ·)) |
33 | 21, 21 | jca 513 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π») β (( I βΎ π) β πΈ β§ ( I βΎ π) β πΈ)) |
34 | 1, 2, 13, 3, 9, 19 | dvamulr 39504 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (( I βΎ π) β πΈ β§ ( I βΎ π) β πΈ)) β (( I βΎ π) Γ ( I βΎ π)) = (( I βΎ π) β ( I βΎ π))) |
35 | 33, 34 | mpdan 686 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β (( I βΎ π) Γ ( I βΎ π)) = (( I βΎ π) β ( I βΎ π))) |
36 | | f1oi 6827 |
. . . . . . . 8
β’ ( I
βΎ π):πβ1-1-ontoβπ |
37 | | f1of 6789 |
. . . . . . . 8
β’ (( I
βΎ π):πβ1-1-ontoβπ β ( I βΎ π):πβΆπ) |
38 | | fcoi2 6722 |
. . . . . . . 8
β’ (( I
βΎ π):πβΆπ β (( I βΎ π) β ( I βΎ π)) = ( I βΎ π)) |
39 | 36, 37, 38 | mp2b 10 |
. . . . . . 7
β’ (( I
βΎ π) β ( I
βΎ π)) = ( I βΎ
π) |
40 | 35, 39 | eqtrdi 2793 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β (( I βΎ π) Γ ( I βΎ π)) = ( I βΎ π)) |
41 | 22, 32, 40 | 3jca 1129 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β (( I βΎ π) β (Baseβπ·) β§ ( I βΎ π) β (0gβπ·) β§ (( I βΎ π) Γ ( I βΎ π)) = ( I βΎ π))) |
42 | 1, 26 | erngdv 39485 |
. . . . . . 7
β’ ((πΎ β HL β§ π β π») β ((EDRingβπΎ)βπ) β DivRing) |
43 | 27, 42 | eqeltrd 2838 |
. . . . . 6
β’ ((πΎ β HL β§ π β π») β π· β DivRing) |
44 | | eqid 2737 |
. . . . . . 7
β’
(0gβπ·) = (0gβπ·) |
45 | | eqid 2737 |
. . . . . . 7
β’
(1rβπ·) = (1rβπ·) |
46 | 14, 19, 44, 45 | drngid2 20218 |
. . . . . 6
β’ (π· β DivRing β ((( I
βΎ π) β
(Baseβπ·) β§ ( I
βΎ π) β
(0gβπ·)
β§ (( I βΎ π) Γ ( I
βΎ π)) = ( I βΎ
π)) β
(1rβπ·) = (
I βΎ π))) |
47 | 43, 46 | syl 17 |
. . . . 5
β’ ((πΎ β HL β§ π β π») β ((( I βΎ π) β (Baseβπ·) β§ ( I βΎ π) β (0gβπ·) β§ (( I βΎ π) Γ ( I βΎ π)) = ( I βΎ π)) β
(1rβπ·) = (
I βΎ π))) |
48 | 41, 47 | mpbid 231 |
. . . 4
β’ ((πΎ β HL β§ π β π») β (1rβπ·) = ( I βΎ π)) |
49 | 48 | eqcomd 2743 |
. . 3
β’ ((πΎ β HL β§ π β π») β ( I βΎ π) = (1rβπ·)) |
50 | | drngring 20206 |
. . . 4
β’ (π· β DivRing β π· β Ring) |
51 | 43, 50 | syl 17 |
. . 3
β’ ((πΎ β HL β§ π β π») β π· β Ring) |
52 | 1, 3 | dvaabl 39516 |
. . . 4
β’ ((πΎ β HL β§ π β π») β π β Abel) |
53 | | ablgrp 19574 |
. . . 4
β’ (π β Abel β π β Grp) |
54 | 52, 53 | syl 17 |
. . 3
β’ ((πΎ β HL β§ π β π») β π β Grp) |
55 | 1, 2, 13, 3, 11 | dvavsca 39509 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π)) β (π Β· π‘) = (π βπ‘)) |
56 | 55 | 3impb 1116 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β π) β (π Β· π‘) = (π βπ‘)) |
57 | 1, 2, 13 | tendocl 39259 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β π) β (π βπ‘) β π) |
58 | 56, 57 | eqeltrd 2838 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β π) β (π Β· π‘) β π) |
59 | 1, 2, 13 | tendospdi1 39512 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β (π β(π‘ β π)) = ((π βπ‘) β (π βπ))) |
60 | | simpr1 1195 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β π β πΈ) |
61 | 1, 2 | ltrnco 39211 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π‘ β π β§ π β π) β (π‘ β π) β π) |
62 | 61 | 3adant3r1 1183 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β (π‘ β π) β π) |
63 | 60, 62 | jca 513 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β (π β πΈ β§ (π‘ β π) β π)) |
64 | 1, 2, 13, 3, 11 | dvavsca 39509 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ (π‘ β π) β π)) β (π Β· (π‘ β π)) = (π β(π‘ β π))) |
65 | 63, 64 | syldan 592 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β (π Β· (π‘ β π)) = (π β(π‘ β π))) |
66 | 57 | 3adant3r3 1185 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β (π βπ‘) β π) |
67 | 1, 2, 13 | tendocl 39259 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (π βπ) β π) |
68 | 67 | 3adant3r2 1184 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β (π βπ) β π) |
69 | 66, 68 | jca 513 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β ((π βπ‘) β π β§ (π βπ) β π)) |
70 | 1, 2, 3, 7 | dvavadd 39507 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π βπ‘) β π β§ (π βπ) β π)) β ((π βπ‘) + (π βπ)) = ((π βπ‘) β (π βπ))) |
71 | 69, 70 | syldan 592 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β ((π βπ‘) + (π βπ)) = ((π βπ‘) β (π βπ))) |
72 | 59, 65, 71 | 3eqtr4d 2787 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β (π Β· (π‘ β π)) = ((π βπ‘) + (π βπ))) |
73 | 1, 2, 3, 7 | dvavadd 39507 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π‘ β π β§ π β π)) β (π‘ + π) = (π‘ β π)) |
74 | 73 | 3adantr1 1170 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β (π‘ + π) = (π‘ β π)) |
75 | 74 | oveq2d 7378 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β (π Β· (π‘ + π)) = (π Β· (π‘ β π))) |
76 | 55 | 3adantr3 1172 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β (π Β· π‘) = (π βπ‘)) |
77 | 1, 2, 13, 3, 11 | dvavsca 39509 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π)) β (π Β· π) = (π βπ)) |
78 | 77 | 3adantr2 1171 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β (π Β· π) = (π βπ)) |
79 | 76, 78 | oveq12d 7380 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β ((π Β· π‘) + (π Β· π)) = ((π βπ‘) + (π βπ))) |
80 | 72, 75, 79 | 3eqtr4d 2787 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β π β§ π β π)) β (π Β· (π‘ + π)) = ((π Β· π‘) + (π Β· π))) |
81 | 1, 2, 13, 3, 9, 17 | dvaplusgv 39502 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π ⨣ π‘)βπ) = ((π βπ) β (π‘βπ))) |
82 | 1, 2, 13, 3, 9, 17 | dvafplusg 39500 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π») β ⨣ = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))) |
83 | 82 | 3ad2ant1 1134 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β πΈ) β ⨣ = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))) |
84 | 83 | oveqd 7379 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β πΈ) β (π ⨣ π‘) = (π (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))π‘)) |
85 | | eqid 2737 |
. . . . . . . . 9
β’ (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) |
86 | 1, 2, 13, 85 | tendoplcl 39273 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β πΈ) β (π (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ))))π‘) β πΈ) |
87 | 84, 86 | eqeltrd 2838 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β πΈ) β (π ⨣ π‘) β πΈ) |
88 | 87 | 3adant3r3 1185 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β (π ⨣ π‘) β πΈ) |
89 | | simpr3 1197 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β π β π) |
90 | 88, 89 | jca 513 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π ⨣ π‘) β πΈ β§ π β π)) |
91 | 1, 2, 13, 3, 11 | dvavsca 39509 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π ⨣ π‘) β πΈ β§ π β π)) β ((π ⨣ π‘) Β· π) = ((π ⨣ π‘)βπ)) |
92 | 90, 91 | syldan 592 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π ⨣ π‘) Β· π) = ((π ⨣ π‘)βπ)) |
93 | 77 | 3adantr2 1171 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β (π Β· π) = (π βπ)) |
94 | 1, 2, 13, 3, 11 | dvavsca 39509 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π‘ β πΈ β§ π β π)) β (π‘ Β· π) = (π‘βπ)) |
95 | 94 | 3adantr1 1170 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β (π‘ Β· π) = (π‘βπ)) |
96 | 93, 95 | oveq12d 7380 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π Β· π) + (π‘ Β· π)) = ((π βπ) + (π‘βπ))) |
97 | 67 | 3adant3r2 1184 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β (π βπ) β π) |
98 | 1, 2, 13 | tendospcl 39510 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π‘ β πΈ β§ π β π) β (π‘βπ) β π) |
99 | 98 | 3adant3r1 1183 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β (π‘βπ) β π) |
100 | 97, 99 | jca 513 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π βπ) β π β§ (π‘βπ) β π)) |
101 | 1, 2, 3, 7 | dvavadd 39507 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π βπ) β π β§ (π‘βπ) β π)) β ((π βπ) + (π‘βπ)) = ((π βπ) β (π‘βπ))) |
102 | 100, 101 | syldan 592 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π βπ) + (π‘βπ)) = ((π βπ) β (π‘βπ))) |
103 | 96, 102 | eqtrd 2777 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π Β· π) + (π‘ Β· π)) = ((π βπ) β (π‘βπ))) |
104 | 81, 92, 103 | 3eqtr4d 2787 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π ⨣ π‘) Β· π) = ((π Β· π) + (π‘ Β· π))) |
105 | 1, 2, 13 | tendospass 39511 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π β π‘)βπ) = (π β(π‘βπ))) |
106 | 1, 13 | tendococl 39264 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π‘ β πΈ) β (π β π‘) β πΈ) |
107 | 106 | 3adant3r3 1185 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β (π β π‘) β πΈ) |
108 | 107, 89 | jca 513 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π β π‘) β πΈ β§ π β π)) |
109 | 1, 2, 13, 3, 11 | dvavsca 39509 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π‘) β πΈ β§ π β π)) β ((π β π‘) Β· π) = ((π β π‘)βπ)) |
110 | 108, 109 | syldan 592 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π β π‘) Β· π) = ((π β π‘)βπ)) |
111 | | simpr1 1195 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β π β πΈ) |
112 | 111, 99 | jca 513 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β (π β πΈ β§ (π‘βπ) β π)) |
113 | 1, 2, 13, 3, 11 | dvavsca 39509 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ (π‘βπ) β π)) β (π Β· (π‘βπ)) = (π β(π‘βπ))) |
114 | 112, 113 | syldan 592 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β (π Β· (π‘βπ)) = (π β(π‘βπ))) |
115 | 105, 110,
114 | 3eqtr4d 2787 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π β π‘) Β· π) = (π Β· (π‘βπ))) |
116 | 1, 2, 13, 3, 9, 19 | dvamulr 39504 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ)) β (π Γ π‘) = (π β π‘)) |
117 | 116 | 3adantr3 1172 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β (π Γ π‘) = (π β π‘)) |
118 | 117 | oveq1d 7377 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π Γ π‘) Β· π) = ((π β π‘) Β· π)) |
119 | 95 | oveq2d 7378 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β (π Β· (π‘ Β· π)) = (π Β· (π‘βπ))) |
120 | 115, 118,
119 | 3eqtr4d 2787 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π‘ β πΈ β§ π β π)) β ((π Γ π‘) Β· π) = (π Β· (π‘ Β· π))) |
121 | 21 | anim1i 616 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ π β π) β (( I βΎ π) β πΈ β§ π β π)) |
122 | 1, 2, 13, 3, 11 | dvavsca 39509 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (( I βΎ π) β πΈ β§ π β π)) β (( I βΎ π) Β· π ) = (( I βΎ π)βπ )) |
123 | 121, 122 | syldan 592 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β (( I βΎ π) Β· π ) = (( I βΎ π)βπ )) |
124 | | fvresi 7124 |
. . . . 5
β’ (π β π β (( I βΎ π)βπ ) = π ) |
125 | 124 | adantl 483 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ π β π) β (( I βΎ π)βπ ) = π ) |
126 | 123, 125 | eqtrd 2777 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ π β π) β (( I βΎ π) Β· π ) = π ) |
127 | 6, 8, 10, 12, 16, 18, 20, 49, 51, 54, 58, 80, 104, 120, 126 | islmodd 20344 |
. 2
β’ ((πΎ β HL β§ π β π») β π β LMod) |
128 | 9 | islvec 20581 |
. 2
β’ (π β LVec β (π β LMod β§ π· β
DivRing)) |
129 | 127, 43, 128 | sylanbrc 584 |
1
β’ ((πΎ β HL β§ π β π») β π β LVec) |