Step | Hyp | Ref
| Expression |
1 | | hdmapglem6.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
2 | | hdmapglem6.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
3 | | hdmapglem6.k |
. . . . . 6
β’ (π β (πΎ β HL β§ π β π»)) |
4 | 1, 2, 3 | dvhlmod 39576 |
. . . . 5
β’ (π β π β LMod) |
5 | | hdmapglem6.r |
. . . . . 6
β’ π
= (Scalarβπ) |
6 | 5 | lmodring 20333 |
. . . . 5
β’ (π β LMod β π
β Ring) |
7 | 4, 6 | syl 17 |
. . . 4
β’ (π β π
β Ring) |
8 | | hdmapglem6.b |
. . . . 5
β’ π΅ = (Baseβπ
) |
9 | | hdmapglem6.g |
. . . . 5
β’ πΊ = ((HGMapβπΎ)βπ) |
10 | | hdmapglem6.x |
. . . . . . 7
β’ (π β π β (π΅ β { 0 })) |
11 | 10 | eldifad 3923 |
. . . . . 6
β’ (π β π β π΅) |
12 | 1, 2, 5, 8, 9, 3, 11 | hgmapcl 40355 |
. . . . 5
β’ (π β (πΊβπ) β π΅) |
13 | 1, 2, 5, 8, 9, 3, 12 | hgmapcl 40355 |
. . . 4
β’ (π β (πΊβ(πΊβπ)) β π΅) |
14 | | hdmapglem6.y |
. . . . . 6
β’ (π β π β (π΅ β { 0 })) |
15 | 14 | eldifad 3923 |
. . . . 5
β’ (π β π β π΅) |
16 | 1, 2, 5, 8, 9, 3, 15 | hgmapcl 40355 |
. . . 4
β’ (π β (πΊβπ) β π΅) |
17 | 1, 2, 3 | dvhlvec 39575 |
. . . . . 6
β’ (π β π β LVec) |
18 | 5 | lvecdrng 20569 |
. . . . . 6
β’ (π β LVec β π
β
DivRing) |
19 | 17, 18 | syl 17 |
. . . . 5
β’ (π β π
β DivRing) |
20 | | eldifsni 4751 |
. . . . . . 7
β’ (π β (π΅ β { 0 }) β π β 0 ) |
21 | 14, 20 | syl 17 |
. . . . . 6
β’ (π β π β 0 ) |
22 | | hdmapglem6.z |
. . . . . . . 8
β’ 0 =
(0gβπ
) |
23 | 1, 2, 5, 8, 22, 9,
3, 15 | hgmapeq0 40370 |
. . . . . . 7
β’ (π β ((πΊβπ) = 0 β π = 0 )) |
24 | 23 | necon3bid 2989 |
. . . . . 6
β’ (π β ((πΊβπ) β 0 β π β 0 )) |
25 | 21, 24 | mpbird 257 |
. . . . 5
β’ (π β (πΊβπ) β 0 ) |
26 | | hdmapglem6.n |
. . . . . 6
β’ π = (invrβπ
) |
27 | 8, 22, 26 | drnginvrcl 20206 |
. . . . 5
β’ ((π
β DivRing β§ (πΊβπ) β π΅ β§ (πΊβπ) β 0 ) β (πβ(πΊβπ)) β π΅) |
28 | 19, 16, 25, 27 | syl3anc 1372 |
. . . 4
β’ (π β (πβ(πΊβπ)) β π΅) |
29 | | hdmapglem6.t |
. . . . 5
β’ Γ =
(.rβπ
) |
30 | 8, 29 | ringass 19985 |
. . . 4
β’ ((π
β Ring β§ ((πΊβ(πΊβπ)) β π΅ β§ (πΊβπ) β π΅ β§ (πβ(πΊβπ)) β π΅)) β (((πΊβ(πΊβπ)) Γ (πΊβπ)) Γ (πβ(πΊβπ))) = ((πΊβ(πΊβπ)) Γ ((πΊβπ) Γ (πβ(πΊβπ))))) |
31 | 7, 13, 16, 28, 30 | syl13anc 1373 |
. . 3
β’ (π β (((πΊβ(πΊβπ)) Γ (πΊβπ)) Γ (πβ(πΊβπ))) = ((πΊβ(πΊβπ)) Γ ((πΊβπ) Γ (πβ(πΊβπ))))) |
32 | | hdmapglem6.i |
. . . . . 6
β’ 1 =
(1rβπ
) |
33 | 8, 22, 29, 32, 26 | drnginvrr 20210 |
. . . . 5
β’ ((π
β DivRing β§ (πΊβπ) β π΅ β§ (πΊβπ) β 0 ) β ((πΊβπ) Γ (πβ(πΊβπ))) = 1 ) |
34 | 19, 16, 25, 33 | syl3anc 1372 |
. . . 4
β’ (π β ((πΊβπ) Γ (πβ(πΊβπ))) = 1 ) |
35 | 34 | oveq2d 7374 |
. . 3
β’ (π β ((πΊβ(πΊβπ)) Γ ((πΊβπ) Γ (πβ(πΊβπ)))) = ((πΊβ(πΊβπ)) Γ 1 )) |
36 | 8, 29, 32 | ringridm 19994 |
. . . 4
β’ ((π
β Ring β§ (πΊβ(πΊβπ)) β π΅) β ((πΊβ(πΊβπ)) Γ 1 ) = (πΊβ(πΊβπ))) |
37 | 7, 13, 36 | syl2anc 585 |
. . 3
β’ (π β ((πΊβ(πΊβπ)) Γ 1 ) = (πΊβ(πΊβπ))) |
38 | 31, 35, 37 | 3eqtrrd 2782 |
. 2
β’ (π β (πΊβ(πΊβπ)) = (((πΊβ(πΊβπ)) Γ (πΊβπ)) Γ (πβ(πΊβπ)))) |
39 | | hdmapglem6.yx |
. . . . . . 7
β’ (π β (π Γ (πΊβπ)) = 1 ) |
40 | 39 | fveq2d 6847 |
. . . . . 6
β’ (π β (πΊβ(π Γ (πΊβπ))) = (πΊβ 1 )) |
41 | 1, 2, 5, 8, 29, 9,
3, 15, 12 | hgmapmul 40361 |
. . . . . 6
β’ (π β (πΊβ(π Γ (πΊβπ))) = ((πΊβ(πΊβπ)) Γ (πΊβπ))) |
42 | 40, 41 | eqtr3d 2779 |
. . . . 5
β’ (π β (πΊβ 1 ) = ((πΊβ(πΊβπ)) Γ (πΊβπ))) |
43 | | hdmapglem6.cd |
. . . . . . 7
β’ (π β ((πβπ·)βπΆ) = 1 ) |
44 | 43 | fveq2d 6847 |
. . . . . 6
β’ (π β (πΊβ((πβπ·)βπΆ)) = (πΊβ 1 )) |
45 | | hdmapglem6.e |
. . . . . . 7
β’ πΈ = β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β© |
46 | | hdmapglem6.o |
. . . . . . 7
β’ π = ((ocHβπΎ)βπ) |
47 | | hdmapglem6.v |
. . . . . . 7
β’ π = (Baseβπ) |
48 | | eqid 2737 |
. . . . . . 7
β’
(+gβπ) = (+gβπ) |
49 | | eqid 2737 |
. . . . . . 7
β’
(-gβπ) = (-gβπ) |
50 | | hdmapglem6.q |
. . . . . . 7
β’ Β· = (
Β·π βπ) |
51 | | hdmapglem6.s |
. . . . . . 7
β’ π = ((HDMapβπΎ)βπ) |
52 | | hdmapglem6.c |
. . . . . . 7
β’ (π β πΆ β (πβ{πΈ})) |
53 | | hdmapglem6.d |
. . . . . . 7
β’ (π β π· β (πβ{πΈ})) |
54 | 1, 45, 46, 2, 47, 48, 49, 50, 5, 8, 29, 22, 51, 9, 3, 52, 53, 15, 11 | hdmapglem5 40388 |
. . . . . 6
β’ (π β (πΊβ((πβπ·)βπΆ)) = ((πβπΆ)βπ·)) |
55 | 44, 54 | eqtr3d 2779 |
. . . . 5
β’ (π β (πΊβ 1 ) = ((πβπΆ)βπ·)) |
56 | 42, 55 | eqtr3d 2779 |
. . . 4
β’ (π β ((πΊβ(πΊβπ)) Γ (πΊβπ)) = ((πβπΆ)βπ·)) |
57 | 39, 43 | eqtr4d 2780 |
. . . . 5
β’ (π β (π Γ (πΊβπ)) = ((πβπ·)βπΆ)) |
58 | 1, 45, 46, 2, 47, 48, 49, 50, 5, 8, 29, 22, 51, 9, 3, 52, 53, 15, 11, 57 | hdmapinvlem4 40387 |
. . . 4
β’ (π β (π Γ (πΊβπ)) = ((πβπΆ)βπ·)) |
59 | 56, 58 | eqtr4d 2780 |
. . 3
β’ (π β ((πΊβ(πΊβπ)) Γ (πΊβπ)) = (π Γ (πΊβπ))) |
60 | 59 | oveq1d 7373 |
. 2
β’ (π β (((πΊβ(πΊβπ)) Γ (πΊβπ)) Γ (πβ(πΊβπ))) = ((π Γ (πΊβπ)) Γ (πβ(πΊβπ)))) |
61 | 8, 29 | ringass 19985 |
. . . 4
β’ ((π
β Ring β§ (π β π΅ β§ (πΊβπ) β π΅ β§ (πβ(πΊβπ)) β π΅)) β ((π Γ (πΊβπ)) Γ (πβ(πΊβπ))) = (π Γ ((πΊβπ) Γ (πβ(πΊβπ))))) |
62 | 7, 11, 16, 28, 61 | syl13anc 1373 |
. . 3
β’ (π β ((π Γ (πΊβπ)) Γ (πβ(πΊβπ))) = (π Γ ((πΊβπ) Γ (πβ(πΊβπ))))) |
63 | 34 | oveq2d 7374 |
. . 3
β’ (π β (π Γ ((πΊβπ) Γ (πβ(πΊβπ)))) = (π Γ 1 )) |
64 | 8, 29, 32 | ringridm 19994 |
. . . 4
β’ ((π
β Ring β§ π β π΅) β (π Γ 1 ) = π) |
65 | 7, 11, 64 | syl2anc 585 |
. . 3
β’ (π β (π Γ 1 ) = π) |
66 | 62, 63, 65 | 3eqtrd 2781 |
. 2
β’ (π β ((π Γ (πΊβπ)) Γ (πβ(πΊβπ))) = π) |
67 | 38, 60, 66 | 3eqtrd 2781 |
1
β’ (π β (πΊβ(πΊβπ)) = π) |