Step | Hyp | Ref
| Expression |
1 | | hdmapinvlem3.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | hdmapinvlem3.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
3 | | hdmapinvlem3.v |
. . . 4
β’ π = (Baseβπ) |
4 | | hdmapinvlem3.m |
. . . 4
β’ β =
(-gβπ) |
5 | | hdmapinvlem3.r |
. . . 4
β’ π
= (Scalarβπ) |
6 | | eqid 2737 |
. . . 4
β’
(-gβπ
) = (-gβπ
) |
7 | | hdmapinvlem3.s |
. . . 4
β’ π = ((HDMapβπΎ)βπ) |
8 | | hdmapinvlem3.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
9 | 1, 2, 8 | dvhlmod 39576 |
. . . . 5
β’ (π β π β LMod) |
10 | | hdmapinvlem3.j |
. . . . 5
β’ (π β π½ β π΅) |
11 | | eqid 2737 |
. . . . . . 7
β’
(BaseβπΎ) =
(BaseβπΎ) |
12 | | eqid 2737 |
. . . . . . 7
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
13 | | eqid 2737 |
. . . . . . 7
β’
(0gβπ) = (0gβπ) |
14 | | hdmapinvlem3.e |
. . . . . . 7
β’ πΈ = β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β© |
15 | 1, 11, 12, 2, 3, 13, 14, 8 | dvheveccl 39578 |
. . . . . 6
β’ (π β πΈ β (π β {(0gβπ)})) |
16 | 15 | eldifad 3923 |
. . . . 5
β’ (π β πΈ β π) |
17 | | hdmapinvlem3.q |
. . . . . 6
β’ Β· = (
Β·π βπ) |
18 | | hdmapinvlem3.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
19 | 3, 5, 17, 18 | lmodvscl 20342 |
. . . . 5
β’ ((π β LMod β§ π½ β π΅ β§ πΈ β π) β (π½ Β· πΈ) β π) |
20 | 9, 10, 16, 19 | syl3anc 1372 |
. . . 4
β’ (π β (π½ Β· πΈ) β π) |
21 | 16 | snssd 4770 |
. . . . . 6
β’ (π β {πΈ} β π) |
22 | | hdmapinvlem3.o |
. . . . . . 7
β’ π = ((ocHβπΎ)βπ) |
23 | 1, 2, 3, 22 | dochssv 39821 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ {πΈ} β π) β (πβ{πΈ}) β π) |
24 | 8, 21, 23 | syl2anc 585 |
. . . . 5
β’ (π β (πβ{πΈ}) β π) |
25 | | hdmapinvlem3.d |
. . . . 5
β’ (π β π· β (πβ{πΈ})) |
26 | 24, 25 | sseldd 3946 |
. . . 4
β’ (π β π· β π) |
27 | | hdmapinvlem3.i |
. . . . . 6
β’ (π β πΌ β π΅) |
28 | 3, 5, 17, 18 | lmodvscl 20342 |
. . . . . 6
β’ ((π β LMod β§ πΌ β π΅ β§ πΈ β π) β (πΌ Β· πΈ) β π) |
29 | 9, 27, 16, 28 | syl3anc 1372 |
. . . . 5
β’ (π β (πΌ Β· πΈ) β π) |
30 | | hdmapinvlem3.c |
. . . . . 6
β’ (π β πΆ β (πβ{πΈ})) |
31 | 24, 30 | sseldd 3946 |
. . . . 5
β’ (π β πΆ β π) |
32 | | hdmapinvlem3.p |
. . . . . 6
β’ + =
(+gβπ) |
33 | 3, 32 | lmodvacl 20339 |
. . . . 5
β’ ((π β LMod β§ (πΌ Β· πΈ) β π β§ πΆ β π) β ((πΌ Β· πΈ) + πΆ) β π) |
34 | 9, 29, 31, 33 | syl3anc 1372 |
. . . 4
β’ (π β ((πΌ Β· πΈ) + πΆ) β π) |
35 | 1, 2, 3, 4, 5, 6, 7, 8, 20, 26, 34 | hdmaplns1 40374 |
. . 3
β’ (π β ((πβ((πΌ Β· πΈ) + πΆ))β((π½ Β· πΈ) β π·)) = (((πβ((πΌ Β· πΈ) + πΆ))β(π½ Β· πΈ))(-gβπ
)((πβ((πΌ Β· πΈ) + πΆ))βπ·))) |
36 | | hdmapinvlem3.t |
. . . . 5
β’ Γ =
(.rβπ
) |
37 | | hdmapinvlem3.z |
. . . . 5
β’ 0 =
(0gβπ
) |
38 | | hdmapinvlem3.g |
. . . . 5
β’ πΊ = ((HGMapβπΎ)βπ) |
39 | | hdmapinvlem3.ij |
. . . . 5
β’ (π β (πΌ Γ (πΊβπ½)) = ((πβπ·)βπΆ)) |
40 | 1, 14, 22, 2, 3, 32, 4, 17, 5, 18, 36, 37, 7, 38, 8, 30, 25, 27, 10, 39 | hdmapinvlem3 40386 |
. . . 4
β’ (π β ((πβ((π½ Β· πΈ) β π·))β((πΌ Β· πΈ) + πΆ)) = 0 ) |
41 | 3, 4 | lmodvsubcl 20370 |
. . . . . 6
β’ ((π β LMod β§ (π½ Β· πΈ) β π β§ π· β π) β ((π½ Β· πΈ) β π·) β π) |
42 | 9, 20, 26, 41 | syl3anc 1372 |
. . . . 5
β’ (π β ((π½ Β· πΈ) β π·) β π) |
43 | 1, 2, 3, 5, 37, 7,
8, 42, 34 | hdmapip0com 40383 |
. . . 4
β’ (π β (((πβ((π½ Β· πΈ) β π·))β((πΌ Β· πΈ) + πΆ)) = 0 β ((πβ((πΌ Β· πΈ) + πΆ))β((π½ Β· πΈ) β π·)) = 0 )) |
44 | 40, 43 | mpbid 231 |
. . 3
β’ (π β ((πβ((πΌ Β· πΈ) + πΆ))β((π½ Β· πΈ) β π·)) = 0 ) |
45 | 1, 2, 3, 17, 5, 18, 36, 7, 8, 16, 34, 10 | hdmaplnm1 40375 |
. . . . 5
β’ (π β ((πβ((πΌ Β· πΈ) + πΆ))β(π½ Β· πΈ)) = (π½ Γ ((πβ((πΌ Β· πΈ) + πΆ))βπΈ))) |
46 | | eqid 2737 |
. . . . . . . 8
β’
(+gβπ
) = (+gβπ
) |
47 | 1, 2, 3, 32, 5, 46, 7, 8, 16, 29, 31 | hdmaplna2 40376 |
. . . . . . 7
β’ (π β ((πβ((πΌ Β· πΈ) + πΆ))βπΈ) = (((πβ(πΌ Β· πΈ))βπΈ)(+gβπ
)((πβπΆ)βπΈ))) |
48 | 1, 14, 22, 2, 3, 5,
18, 36, 37, 7, 8, 30 | hdmapinvlem2 40385 |
. . . . . . . 8
β’ (π β ((πβπΆ)βπΈ) = 0 ) |
49 | 48 | oveq2d 7374 |
. . . . . . 7
β’ (π β (((πβ(πΌ Β· πΈ))βπΈ)(+gβπ
)((πβπΆ)βπΈ)) = (((πβ(πΌ Β· πΈ))βπΈ)(+gβπ
) 0 )) |
50 | 5 | lmodring 20333 |
. . . . . . . . . . 11
β’ (π β LMod β π
β Ring) |
51 | 9, 50 | syl 17 |
. . . . . . . . . 10
β’ (π β π
β Ring) |
52 | | ringgrp 19970 |
. . . . . . . . . 10
β’ (π
β Ring β π
β Grp) |
53 | 51, 52 | syl 17 |
. . . . . . . . 9
β’ (π β π
β Grp) |
54 | 1, 2, 3, 5, 18, 7,
8, 16, 29 | hdmapipcl 40371 |
. . . . . . . . 9
β’ (π β ((πβ(πΌ Β· πΈ))βπΈ) β π΅) |
55 | 18, 46, 37 | grprid 18782 |
. . . . . . . . 9
β’ ((π
β Grp β§ ((πβ(πΌ Β· πΈ))βπΈ) β π΅) β (((πβ(πΌ Β· πΈ))βπΈ)(+gβπ
) 0 ) = ((πβ(πΌ Β· πΈ))βπΈ)) |
56 | 53, 54, 55 | syl2anc 585 |
. . . . . . . 8
β’ (π β (((πβ(πΌ Β· πΈ))βπΈ)(+gβπ
) 0 ) = ((πβ(πΌ Β· πΈ))βπΈ)) |
57 | 1, 2, 3, 17, 5, 18, 36, 7, 38, 8, 16, 16, 27 | hdmapglnm2 40377 |
. . . . . . . 8
β’ (π β ((πβ(πΌ Β· πΈ))βπΈ) = (((πβπΈ)βπΈ) Γ (πΊβπΌ))) |
58 | | eqid 2737 |
. . . . . . . . . . 11
β’
((HVMapβπΎ)βπ) = ((HVMapβπΎ)βπ) |
59 | | eqid 2737 |
. . . . . . . . . . 11
β’
(1rβπ
) = (1rβπ
) |
60 | 1, 14, 58, 7, 8, 2,
5, 59 | hdmapevec2 40302 |
. . . . . . . . . 10
β’ (π β ((πβπΈ)βπΈ) = (1rβπ
)) |
61 | 60 | oveq1d 7373 |
. . . . . . . . 9
β’ (π β (((πβπΈ)βπΈ) Γ (πΊβπΌ)) = ((1rβπ
) Γ (πΊβπΌ))) |
62 | 1, 2, 5, 18, 38, 8, 27 | hgmapcl 40355 |
. . . . . . . . . 10
β’ (π β (πΊβπΌ) β π΅) |
63 | 18, 36, 59 | ringlidm 19993 |
. . . . . . . . . 10
β’ ((π
β Ring β§ (πΊβπΌ) β π΅) β ((1rβπ
) Γ (πΊβπΌ)) = (πΊβπΌ)) |
64 | 51, 62, 63 | syl2anc 585 |
. . . . . . . . 9
β’ (π β
((1rβπ
)
Γ
(πΊβπΌ)) = (πΊβπΌ)) |
65 | 61, 64 | eqtrd 2777 |
. . . . . . . 8
β’ (π β (((πβπΈ)βπΈ) Γ (πΊβπΌ)) = (πΊβπΌ)) |
66 | 56, 57, 65 | 3eqtrd 2781 |
. . . . . . 7
β’ (π β (((πβ(πΌ Β· πΈ))βπΈ)(+gβπ
) 0 ) = (πΊβπΌ)) |
67 | 47, 49, 66 | 3eqtrd 2781 |
. . . . . 6
β’ (π β ((πβ((πΌ Β· πΈ) + πΆ))βπΈ) = (πΊβπΌ)) |
68 | 67 | oveq2d 7374 |
. . . . 5
β’ (π β (π½ Γ ((πβ((πΌ Β· πΈ) + πΆ))βπΈ)) = (π½ Γ (πΊβπΌ))) |
69 | 45, 68 | eqtrd 2777 |
. . . 4
β’ (π β ((πβ((πΌ Β· πΈ) + πΆ))β(π½ Β· πΈ)) = (π½ Γ (πΊβπΌ))) |
70 | 1, 2, 3, 32, 5, 46, 7, 8, 26, 29, 31 | hdmaplna2 40376 |
. . . . 5
β’ (π β ((πβ((πΌ Β· πΈ) + πΆ))βπ·) = (((πβ(πΌ Β· πΈ))βπ·)(+gβπ
)((πβπΆ)βπ·))) |
71 | 1, 2, 3, 17, 5, 18, 36, 7, 38, 8, 26, 16, 27 | hdmapglnm2 40377 |
. . . . . . 7
β’ (π β ((πβ(πΌ Β· πΈ))βπ·) = (((πβπΈ)βπ·) Γ (πΊβπΌ))) |
72 | 1, 14, 22, 2, 3, 5,
18, 36, 37, 7, 8, 25 | hdmapinvlem1 40384 |
. . . . . . . 8
β’ (π β ((πβπΈ)βπ·) = 0 ) |
73 | 72 | oveq1d 7373 |
. . . . . . 7
β’ (π β (((πβπΈ)βπ·) Γ (πΊβπΌ)) = ( 0 Γ (πΊβπΌ))) |
74 | 18, 36, 37 | ringlz 20012 |
. . . . . . . 8
β’ ((π
β Ring β§ (πΊβπΌ) β π΅) β ( 0 Γ (πΊβπΌ)) = 0 ) |
75 | 51, 62, 74 | syl2anc 585 |
. . . . . . 7
β’ (π β ( 0 Γ (πΊβπΌ)) = 0 ) |
76 | 71, 73, 75 | 3eqtrd 2781 |
. . . . . 6
β’ (π β ((πβ(πΌ Β· πΈ))βπ·) = 0 ) |
77 | 76 | oveq1d 7373 |
. . . . 5
β’ (π β (((πβ(πΌ Β· πΈ))βπ·)(+gβπ
)((πβπΆ)βπ·)) = ( 0 (+gβπ
)((πβπΆ)βπ·))) |
78 | 1, 2, 3, 5, 18, 7,
8, 26, 31 | hdmapipcl 40371 |
. . . . . 6
β’ (π β ((πβπΆ)βπ·) β π΅) |
79 | 18, 46, 37 | grplid 18781 |
. . . . . 6
β’ ((π
β Grp β§ ((πβπΆ)βπ·) β π΅) β ( 0 (+gβπ
)((πβπΆ)βπ·)) = ((πβπΆ)βπ·)) |
80 | 53, 78, 79 | syl2anc 585 |
. . . . 5
β’ (π β ( 0 (+gβπ
)((πβπΆ)βπ·)) = ((πβπΆ)βπ·)) |
81 | 70, 77, 80 | 3eqtrd 2781 |
. . . 4
β’ (π β ((πβ((πΌ Β· πΈ) + πΆ))βπ·) = ((πβπΆ)βπ·)) |
82 | 69, 81 | oveq12d 7376 |
. . 3
β’ (π β (((πβ((πΌ Β· πΈ) + πΆ))β(π½ Β· πΈ))(-gβπ
)((πβ((πΌ Β· πΈ) + πΆ))βπ·)) = ((π½ Γ (πΊβπΌ))(-gβπ
)((πβπΆ)βπ·))) |
83 | 35, 44, 82 | 3eqtr3rd 2786 |
. 2
β’ (π β ((π½ Γ (πΊβπΌ))(-gβπ
)((πβπΆ)βπ·)) = 0 ) |
84 | 5, 18, 36 | lmodmcl 20337 |
. . . 4
β’ ((π β LMod β§ π½ β π΅ β§ (πΊβπΌ) β π΅) β (π½ Γ (πΊβπΌ)) β π΅) |
85 | 9, 10, 62, 84 | syl3anc 1372 |
. . 3
β’ (π β (π½ Γ (πΊβπΌ)) β π΅) |
86 | 18, 37, 6 | grpsubeq0 18834 |
. . 3
β’ ((π
β Grp β§ (π½ Γ (πΊβπΌ)) β π΅ β§ ((πβπΆ)βπ·) β π΅) β (((π½ Γ (πΊβπΌ))(-gβπ
)((πβπΆ)βπ·)) = 0 β (π½ Γ (πΊβπΌ)) = ((πβπΆ)βπ·))) |
87 | 53, 85, 78, 86 | syl3anc 1372 |
. 2
β’ (π β (((π½ Γ (πΊβπΌ))(-gβπ
)((πβπΆ)βπ·)) = 0 β (π½ Γ (πΊβπΌ)) = ((πβπΆ)βπ·))) |
88 | 83, 87 | mpbid 231 |
1
β’ (π β (π½ Γ (πΊβπΌ)) = ((πβπΆ)βπ·)) |