Step | Hyp | Ref
| Expression |
1 | | hdmapglem7.h |
. . 3
β’ π» = (LHypβπΎ) |
2 | | hdmapglem7.e |
. . 3
β’ πΈ = β¨( I βΎ
(BaseβπΎ)), ( I
βΎ ((LTrnβπΎ)βπ))β© |
3 | | hdmapglem7.o |
. . 3
β’ π = ((ocHβπΎ)βπ) |
4 | | hdmapglem7.u |
. . 3
β’ π = ((DVecHβπΎ)βπ) |
5 | | hdmapglem7.v |
. . 3
β’ π = (Baseβπ) |
6 | | hdmapglem7.p |
. . 3
β’ + =
(+gβπ) |
7 | | hdmapglem7.q |
. . 3
β’ Β· = (
Β·π βπ) |
8 | | hdmapglem7.r |
. . 3
β’ π
= (Scalarβπ) |
9 | | hdmapglem7.b |
. . 3
β’ π΅ = (Baseβπ
) |
10 | | hdmapglem7.a |
. . 3
β’ β =
(LSSumβπ) |
11 | | hdmapglem7.n |
. . 3
β’ π = (LSpanβπ) |
12 | | hdmapglem7.k |
. . 3
β’ (π β (πΎ β HL β§ π β π»)) |
13 | | hdmapglem7.x |
. . 3
β’ (π β π β π) |
14 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 13 | hdmapglem7a 40736 |
. 2
β’ (π β βπ’ β (πβ{πΈ})βπ β π΅ π = ((π Β· πΈ) + π’)) |
15 | | hdmapglem7.y |
. . 3
β’ (π β π β π) |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 12, 15 | hdmapglem7a 40736 |
. 2
β’ (π β βπ£ β (πβ{πΈ})βπ β π΅ π = ((π Β· πΈ) + π£)) |
17 | | hdmapglem7.c |
. . . . . . . . . . . 12
β’ β =
(+gβπ
) |
18 | | hdmapglem7.g |
. . . . . . . . . . . 12
β’ πΊ = ((HGMapβπΎ)βπ) |
19 | 12 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (πΎ β HL β§ π β π»)) |
20 | 1, 4, 12 | dvhlmod 39919 |
. . . . . . . . . . . . . . 15
β’ (π β π β LMod) |
21 | 8 | lmodring 20467 |
. . . . . . . . . . . . . . 15
β’ (π β LMod β π
β Ring) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β π
β Ring) |
23 | 22 | ad2antrr 725 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β π
β Ring) |
24 | | simplrr 777 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β π β π΅) |
25 | | simprr 772 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β π β π΅) |
26 | 1, 4, 8, 9, 18, 19, 25 | hgmapcl 40698 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (πΊβπ) β π΅) |
27 | | hdmapglem7.t |
. . . . . . . . . . . . . 14
β’ Γ =
(.rβπ
) |
28 | 9, 27 | ringcl 20064 |
. . . . . . . . . . . . 13
β’ ((π
β Ring β§ π β π΅ β§ (πΊβπ) β π΅) β (π Γ (πΊβπ)) β π΅) |
29 | 23, 24, 26, 28 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (π Γ (πΊβπ)) β π΅) |
30 | | hdmapglem7.s |
. . . . . . . . . . . . 13
β’ π = ((HDMapβπΎ)βπ) |
31 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(BaseβπΎ) =
(BaseβπΎ) |
32 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
((LTrnβπΎ)βπ) = ((LTrnβπΎ)βπ) |
33 | | eqid 2733 |
. . . . . . . . . . . . . . . . . . 19
β’
(0gβπ) = (0gβπ) |
34 | 1, 31, 32, 4, 5, 33, 2, 12 | dvheveccl 39921 |
. . . . . . . . . . . . . . . . . 18
β’ (π β πΈ β (π β {(0gβπ)})) |
35 | 34 | eldifad 3959 |
. . . . . . . . . . . . . . . . 17
β’ (π β πΈ β π) |
36 | 35 | snssd 4811 |
. . . . . . . . . . . . . . . 16
β’ (π β {πΈ} β π) |
37 | 1, 4, 5, 3 | dochssv 40164 |
. . . . . . . . . . . . . . . 16
β’ (((πΎ β HL β§ π β π») β§ {πΈ} β π) β (πβ{πΈ}) β π) |
38 | 12, 36, 37 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β (πβ{πΈ}) β π) |
39 | 38 | ad2antrr 725 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (πβ{πΈ}) β π) |
40 | | simplrl 776 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β π’ β (πβ{πΈ})) |
41 | 39, 40 | sseldd 3982 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β π’ β π) |
42 | | simprl 770 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β π£ β (πβ{πΈ})) |
43 | 39, 42 | sseldd 3982 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β π£ β π) |
44 | 1, 4, 5, 8, 9, 30,
19, 41, 43 | hdmapipcl 40714 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β ((πβπ£)βπ’) β π΅) |
45 | 1, 4, 8, 9, 17, 18, 19, 29, 44 | hgmapadd 40703 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (πΊβ((π Γ (πΊβπ)) β ((πβπ£)βπ’))) = ((πΊβ(π Γ (πΊβπ))) β (πΊβ((πβπ£)βπ’)))) |
46 | 1, 4, 8, 9, 27, 18, 19, 24, 26 | hgmapmul 40704 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (πΊβ(π Γ (πΊβπ))) = ((πΊβ(πΊβπ)) Γ (πΊβπ))) |
47 | 1, 4, 8, 9, 18, 19, 25 | hgmapvv 40735 |
. . . . . . . . . . . . . 14
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (πΊβ(πΊβπ)) = π) |
48 | 47 | oveq1d 7419 |
. . . . . . . . . . . . 13
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β ((πΊβ(πΊβπ)) Γ (πΊβπ)) = (π Γ (πΊβπ))) |
49 | 46, 48 | eqtrd 2773 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (πΊβ(π Γ (πΊβπ))) = (π Γ (πΊβπ))) |
50 | | eqid 2733 |
. . . . . . . . . . . . 13
β’
(-gβπ) = (-gβπ) |
51 | | hdmapglem7.z |
. . . . . . . . . . . . 13
β’ 0 =
(0gβπ
) |
52 | 1, 2, 3, 4, 5, 6, 50, 7, 8, 9,
27, 51, 30, 18, 19, 40, 42, 24, 24 | hdmapglem5 40731 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (πΊβ((πβπ£)βπ’)) = ((πβπ’)βπ£)) |
53 | 49, 52 | oveq12d 7422 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β ((πΊβ(π Γ (πΊβπ))) β (πΊβ((πβπ£)βπ’))) = ((π Γ (πΊβπ)) β ((πβπ’)βπ£))) |
54 | 45, 53 | eqtrd 2773 |
. . . . . . . . . 10
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (πΊβ((π Γ (πΊβπ)) β ((πβπ£)βπ’))) = ((π Γ (πΊβπ)) β ((πβπ’)βπ£))) |
55 | 13 | ad2antrr 725 |
. . . . . . . . . . . 12
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β π β π) |
56 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 19, 55, 27, 51, 17, 30, 18, 42, 40, 25, 24 | hdmapglem7b 40737 |
. . . . . . . . . . 11
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β ((πβ((π Β· πΈ) + π£))β((π Β· πΈ) + π’)) = ((π Γ (πΊβπ)) β ((πβπ£)βπ’))) |
57 | 56 | fveq2d 6892 |
. . . . . . . . . 10
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (πΊβ((πβ((π Β· πΈ) + π£))β((π Β· πΈ) + π’))) = (πΊβ((π Γ (πΊβπ)) β ((πβπ£)βπ’)))) |
58 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10,
11, 19, 55, 27, 51, 17, 30, 18, 40, 42, 24, 25 | hdmapglem7b 40737 |
. . . . . . . . . 10
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β ((πβ((π Β· πΈ) + π’))β((π Β· πΈ) + π£)) = ((π Γ (πΊβπ)) β ((πβπ’)βπ£))) |
59 | 54, 57, 58 | 3eqtr4d 2783 |
. . . . . . . . 9
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (πΊβ((πβ((π Β· πΈ) + π£))β((π Β· πΈ) + π’))) = ((πβ((π Β· πΈ) + π’))β((π Β· πΈ) + π£))) |
60 | 59 | 3adantl3 1169 |
. . . . . . . 8
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π’)) β§ (π£ β (πβ{πΈ}) β§ π β π΅)) β (πΊβ((πβ((π Β· πΈ) + π£))β((π Β· πΈ) + π’))) = ((πβ((π Β· πΈ) + π’))β((π Β· πΈ) + π£))) |
61 | 60 | 3adant3 1133 |
. . . . . . 7
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π’)) β§ (π£ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π£)) β (πΊβ((πβ((π Β· πΈ) + π£))β((π Β· πΈ) + π’))) = ((πβ((π Β· πΈ) + π’))β((π Β· πΈ) + π£))) |
62 | | simp3 1139 |
. . . . . . . . . 10
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π’)) β§ (π£ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π£)) β π = ((π Β· πΈ) + π£)) |
63 | 62 | fveq2d 6892 |
. . . . . . . . 9
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π’)) β§ (π£ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π£)) β (πβπ) = (πβ((π Β· πΈ) + π£))) |
64 | | simp13 1206 |
. . . . . . . . 9
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π’)) β§ (π£ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π£)) β π = ((π Β· πΈ) + π’)) |
65 | 63, 64 | fveq12d 6895 |
. . . . . . . 8
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π’)) β§ (π£ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π£)) β ((πβπ)βπ) = ((πβ((π Β· πΈ) + π£))β((π Β· πΈ) + π’))) |
66 | 65 | fveq2d 6892 |
. . . . . . 7
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π’)) β§ (π£ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π£)) β (πΊβ((πβπ)βπ)) = (πΊβ((πβ((π Β· πΈ) + π£))β((π Β· πΈ) + π’)))) |
67 | 64 | fveq2d 6892 |
. . . . . . . 8
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π’)) β§ (π£ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π£)) β (πβπ) = (πβ((π Β· πΈ) + π’))) |
68 | 67, 62 | fveq12d 6895 |
. . . . . . 7
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π’)) β§ (π£ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π£)) β ((πβπ)βπ) = ((πβ((π Β· πΈ) + π’))β((π Β· πΈ) + π£))) |
69 | 61, 66, 68 | 3eqtr4d 2783 |
. . . . . 6
β’ (((π β§ (π’ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π’)) β§ (π£ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π£)) β (πΊβ((πβπ)βπ)) = ((πβπ)βπ)) |
70 | 69 | 3exp 1120 |
. . . . 5
β’ ((π β§ (π’ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π’)) β ((π£ β (πβ{πΈ}) β§ π β π΅) β (π = ((π Β· πΈ) + π£) β (πΊβ((πβπ)βπ)) = ((πβπ)βπ)))) |
71 | 70 | rexlimdvv 3211 |
. . . 4
β’ ((π β§ (π’ β (πβ{πΈ}) β§ π β π΅) β§ π = ((π Β· πΈ) + π’)) β (βπ£ β (πβ{πΈ})βπ β π΅ π = ((π Β· πΈ) + π£) β (πΊβ((πβπ)βπ)) = ((πβπ)βπ))) |
72 | 71 | 3exp 1120 |
. . 3
β’ (π β ((π’ β (πβ{πΈ}) β§ π β π΅) β (π = ((π Β· πΈ) + π’) β (βπ£ β (πβ{πΈ})βπ β π΅ π = ((π Β· πΈ) + π£) β (πΊβ((πβπ)βπ)) = ((πβπ)βπ))))) |
73 | 72 | rexlimdvv 3211 |
. 2
β’ (π β (βπ’ β (πβ{πΈ})βπ β π΅ π = ((π Β· πΈ) + π’) β (βπ£ β (πβ{πΈ})βπ β π΅ π = ((π Β· πΈ) + π£) β (πΊβ((πβπ)βπ)) = ((πβπ)βπ)))) |
74 | 14, 16, 73 | mp2d 49 |
1
β’ (π β (πΊβ((πβπ)βπ)) = ((πβπ)βπ)) |