Step | Hyp | Ref
| Expression |
1 | | fvoveq1 7381 |
. . . 4
β’ (πΉ = (0gβπ
) β (πβ(πΉ Β· π)) = (πβ((0gβπ
) Β· π))) |
2 | 1 | eqeq1d 2739 |
. . 3
β’ (πΉ = (0gβπ
) β ((πβ(πΉ Β· π)) = (π β (πβπ)) β (πβ((0gβπ
) Β· π)) = (π β (πβπ)))) |
3 | 2 | rexbidv 3176 |
. 2
β’ (πΉ = (0gβπ
) β (βπ β π΄ (πβ(πΉ Β· π)) = (π β (πβπ)) β βπ β π΄ (πβ((0gβπ
) Β· π)) = (π β (πβπ)))) |
4 | | difss 4092 |
. . 3
β’ (π΄ β
{(0gβπ)})
β π΄ |
5 | | hdmap14lem1a.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
6 | | hdmap14lem1a.u |
. . . . . 6
β’ π = ((DVecHβπΎ)βπ) |
7 | | hdmap14lem1a.v |
. . . . . 6
β’ π = (Baseβπ) |
8 | | hdmap14lem1a.t |
. . . . . 6
β’ Β· = (
Β·π βπ) |
9 | | hdmap14lem1a.r |
. . . . . 6
β’ π
= (Scalarβπ) |
10 | | hdmap14lem1a.b |
. . . . . 6
β’ π΅ = (Baseβπ
) |
11 | | hdmap14lem1a.c |
. . . . . 6
β’ πΆ = ((LCDualβπΎ)βπ) |
12 | | hdmap14lem2a.e |
. . . . . 6
β’ β = (
Β·π βπΆ) |
13 | | hdmap14lem1a.l |
. . . . . 6
β’ πΏ = (LSpanβπΆ) |
14 | | hdmap14lem2a.p |
. . . . . 6
β’ π = (ScalarβπΆ) |
15 | | hdmap14lem2a.a |
. . . . . 6
β’ π΄ = (Baseβπ) |
16 | | hdmap14lem1a.s |
. . . . . 6
β’ π = ((HDMapβπΎ)βπ) |
17 | | hdmap14lem1a.k |
. . . . . . 7
β’ (π β (πΎ β HL β§ π β π»)) |
18 | 17 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ β (0gβπ
)) β (πΎ β HL β§ π β π»)) |
19 | | hdmap14lem3a.x |
. . . . . . 7
β’ (π β π β π) |
20 | 19 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ β (0gβπ
)) β π β π) |
21 | | hdmap14lem1a.f |
. . . . . . 7
β’ (π β πΉ β π΅) |
22 | 21 | adantr 482 |
. . . . . 6
β’ ((π β§ πΉ β (0gβπ
)) β πΉ β π΅) |
23 | | eqid 2737 |
. . . . . 6
β’
(0gβπ
) = (0gβπ
) |
24 | | simpr 486 |
. . . . . 6
β’ ((π β§ πΉ β (0gβπ
)) β πΉ β (0gβπ
)) |
25 | 5, 6, 7, 8, 9, 10,
11, 12, 13, 14, 15, 16, 18, 20, 22, 23, 24 | hdmap14lem1a 40332 |
. . . . 5
β’ ((π β§ πΉ β (0gβπ
)) β (πΏβ{(πβπ)}) = (πΏβ{(πβ(πΉ Β· π))})) |
26 | 25 | eqcomd 2743 |
. . . 4
β’ ((π β§ πΉ β (0gβπ
)) β (πΏβ{(πβ(πΉ Β· π))}) = (πΏβ{(πβπ)})) |
27 | | eqid 2737 |
. . . . . 6
β’
(BaseβπΆ) =
(BaseβπΆ) |
28 | | eqid 2737 |
. . . . . 6
β’
(0gβπ) = (0gβπ) |
29 | 5, 11, 17 | lcdlvec 40057 |
. . . . . 6
β’ (π β πΆ β LVec) |
30 | 5, 6, 17 | dvhlmod 39576 |
. . . . . . . 8
β’ (π β π β LMod) |
31 | 7, 9, 8, 10 | lmodvscl 20342 |
. . . . . . . 8
β’ ((π β LMod β§ πΉ β π΅ β§ π β π) β (πΉ Β· π) β π) |
32 | 30, 21, 19, 31 | syl3anc 1372 |
. . . . . . 7
β’ (π β (πΉ Β· π) β π) |
33 | 5, 6, 7, 11, 27, 16, 17, 32 | hdmapcl 40296 |
. . . . . 6
β’ (π β (πβ(πΉ Β· π)) β (BaseβπΆ)) |
34 | 5, 6, 7, 11, 27, 16, 17, 19 | hdmapcl 40296 |
. . . . . 6
β’ (π β (πβπ) β (BaseβπΆ)) |
35 | 27, 14, 15, 28, 12, 13, 29, 33, 34 | lspsneq 20586 |
. . . . 5
β’ (π β ((πΏβ{(πβ(πΉ Β· π))}) = (πΏβ{(πβπ)}) β βπ β (π΄ β {(0gβπ)})(πβ(πΉ Β· π)) = (π β (πβπ)))) |
36 | 35 | adantr 482 |
. . . 4
β’ ((π β§ πΉ β (0gβπ
)) β ((πΏβ{(πβ(πΉ Β· π))}) = (πΏβ{(πβπ)}) β βπ β (π΄ β {(0gβπ)})(πβ(πΉ Β· π)) = (π β (πβπ)))) |
37 | 26, 36 | mpbid 231 |
. . 3
β’ ((π β§ πΉ β (0gβπ
)) β βπ β (π΄ β {(0gβπ)})(πβ(πΉ Β· π)) = (π β (πβπ))) |
38 | | ssrexv 4012 |
. . 3
β’ ((π΄ β
{(0gβπ)})
β π΄ β
(βπ β (π΄ β
{(0gβπ)})(πβ(πΉ Β· π)) = (π β (πβπ)) β βπ β π΄ (πβ(πΉ Β· π)) = (π β (πβπ)))) |
39 | 4, 37, 38 | mpsyl 68 |
. 2
β’ ((π β§ πΉ β (0gβπ
)) β βπ β π΄ (πβ(πΉ Β· π)) = (π β (πβπ))) |
40 | 5, 11, 17 | lcdlmod 40058 |
. . . 4
β’ (π β πΆ β LMod) |
41 | 14, 15, 28 | lmod0cl 20351 |
. . . 4
β’ (πΆ β LMod β
(0gβπ)
β π΄) |
42 | 40, 41 | syl 17 |
. . 3
β’ (π β (0gβπ) β π΄) |
43 | | eqid 2737 |
. . . . 5
β’
(0gβπ) = (0gβπ) |
44 | | eqid 2737 |
. . . . 5
β’
(0gβπΆ) = (0gβπΆ) |
45 | 5, 6, 43, 11, 44, 16, 17 | hdmapval0 40299 |
. . . 4
β’ (π β (πβ(0gβπ)) = (0gβπΆ)) |
46 | 7, 9, 8, 23, 43 | lmod0vs 20358 |
. . . . . 6
β’ ((π β LMod β§ π β π) β ((0gβπ
) Β· π) = (0gβπ)) |
47 | 30, 19, 46 | syl2anc 585 |
. . . . 5
β’ (π β
((0gβπ
)
Β·
π) =
(0gβπ)) |
48 | 47 | fveq2d 6847 |
. . . 4
β’ (π β (πβ((0gβπ
) Β· π)) = (πβ(0gβπ))) |
49 | 27, 14, 12, 28, 44 | lmod0vs 20358 |
. . . . 5
β’ ((πΆ β LMod β§ (πβπ) β (BaseβπΆ)) β ((0gβπ) β (πβπ)) = (0gβπΆ)) |
50 | 40, 34, 49 | syl2anc 585 |
. . . 4
β’ (π β
((0gβπ)
β
(πβπ)) = (0gβπΆ)) |
51 | 45, 48, 50 | 3eqtr4d 2787 |
. . 3
β’ (π β (πβ((0gβπ
) Β· π)) = ((0gβπ) β (πβπ))) |
52 | | oveq1 7365 |
. . . 4
β’ (π = (0gβπ) β (π β (πβπ)) = ((0gβπ) β (πβπ))) |
53 | 52 | rspceeqv 3596 |
. . 3
β’
(((0gβπ) β π΄ β§ (πβ((0gβπ
) Β· π)) = ((0gβπ) β (πβπ))) β βπ β π΄ (πβ((0gβπ
) Β· π)) = (π β (πβπ))) |
54 | 42, 51, 53 | syl2anc 585 |
. 2
β’ (π β βπ β π΄ (πβ((0gβπ
) Β· π)) = (π β (πβπ))) |
55 | 3, 39, 54 | pm2.61ne 3031 |
1
β’ (π β βπ β π΄ (πβ(πΉ Β· π)) = (π β (πβπ))) |