Step | Hyp | Ref
| Expression |
1 | | hgmapval0.h |
. . . 4
β’ π» = (LHypβπΎ) |
2 | | hgmapval0.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
3 | | eqid 2737 |
. . . 4
β’
(Baseβπ) =
(Baseβπ) |
4 | | eqid 2737 |
. . . 4
β’
(0gβπ) = (0gβπ) |
5 | | hgmapval0.k |
. . . 4
β’ (π β (πΎ β HL β§ π β π»)) |
6 | 1, 2, 3, 4, 5 | dvh1dim 39908 |
. . 3
β’ (π β βπ₯ β (Baseβπ)π₯ β (0gβπ)) |
7 | | eqid 2737 |
. . . . . . . . 9
β’
((LCDualβπΎ)βπ) = ((LCDualβπΎ)βπ) |
8 | | eqid 2737 |
. . . . . . . . 9
β’
(0gβ((LCDualβπΎ)βπ)) =
(0gβ((LCDualβπΎ)βπ)) |
9 | | eqid 2737 |
. . . . . . . . 9
β’
((HDMapβπΎ)βπ) = ((HDMapβπΎ)βπ) |
10 | 5 | adantr 482 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ)) β (πΎ β HL β§ π β π»)) |
11 | | simpr 486 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ)) β π₯ β (Baseβπ)) |
12 | 1, 2, 3, 4, 7, 8, 9, 10, 11 | hdmapeq0 40310 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ)) β ((((HDMapβπΎ)βπ)βπ₯) = (0gβ((LCDualβπΎ)βπ)) β π₯ = (0gβπ))) |
13 | 12 | biimpd 228 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ)) β ((((HDMapβπΎ)βπ)βπ₯) = (0gβ((LCDualβπΎ)βπ)) β π₯ = (0gβπ))) |
14 | 13 | necon3ad 2957 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ)) β (π₯ β (0gβπ) β Β¬ (((HDMapβπΎ)βπ)βπ₯) = (0gβ((LCDualβπΎ)βπ)))) |
15 | 14 | 3impia 1118 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ) β§ π₯ β (0gβπ)) β Β¬ (((HDMapβπΎ)βπ)βπ₯) = (0gβ((LCDualβπΎ)βπ))) |
16 | 1, 2, 5 | dvhlmod 39576 |
. . . . . . . . . . . 12
β’ (π β π β LMod) |
17 | | hgmapval0.r |
. . . . . . . . . . . . 13
β’ π
= (Scalarβπ) |
18 | | eqid 2737 |
. . . . . . . . . . . . 13
β’ (
Β·π βπ) = ( Β·π
βπ) |
19 | | hgmapval0.o |
. . . . . . . . . . . . 13
β’ 0 =
(0gβπ
) |
20 | 3, 17, 18, 19, 4 | lmod0vs 20358 |
. . . . . . . . . . . 12
β’ ((π β LMod β§ π₯ β (Baseβπ)) β ( 0 (
Β·π βπ)π₯) = (0gβπ)) |
21 | 16, 20 | sylan 581 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (Baseβπ)) β ( 0 (
Β·π βπ)π₯) = (0gβπ)) |
22 | 21 | fveq2d 6847 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β (((HDMapβπΎ)βπ)β( 0 (
Β·π βπ)π₯)) = (((HDMapβπΎ)βπ)β(0gβπ))) |
23 | | eqid 2737 |
. . . . . . . . . . 11
β’
(Baseβπ
) =
(Baseβπ
) |
24 | | eqid 2737 |
. . . . . . . . . . 11
β’ (
Β·π β((LCDualβπΎ)βπ)) = ( Β·π
β((LCDualβπΎ)βπ)) |
25 | | hgmapval0.g |
. . . . . . . . . . 11
β’ πΊ = ((HGMapβπΎ)βπ) |
26 | 17, 23, 19 | lmod0cl 20351 |
. . . . . . . . . . . . 13
β’ (π β LMod β 0 β
(Baseβπ
)) |
27 | 16, 26 | syl 17 |
. . . . . . . . . . . 12
β’ (π β 0 β (Baseβπ
)) |
28 | 27 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (Baseβπ)) β 0 β (Baseβπ
)) |
29 | 1, 2, 3, 18, 17, 23, 7, 24, 9, 25, 10, 11, 28 | hgmapvs 40357 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β (((HDMapβπΎ)βπ)β( 0 (
Β·π βπ)π₯)) = ((πΊβ 0 )(
Β·π β((LCDualβπΎ)βπ))(((HDMapβπΎ)βπ)βπ₯))) |
30 | 1, 2, 4, 7, 8, 9, 5 | hdmapval0 40299 |
. . . . . . . . . . 11
β’ (π β (((HDMapβπΎ)βπ)β(0gβπ)) =
(0gβ((LCDualβπΎ)βπ))) |
31 | 30 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β (((HDMapβπΎ)βπ)β(0gβπ)) =
(0gβ((LCDualβπΎ)βπ))) |
32 | 22, 29, 31 | 3eqtr3d 2785 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ)) β ((πΊβ 0 )(
Β·π β((LCDualβπΎ)βπ))(((HDMapβπΎ)βπ)βπ₯)) =
(0gβ((LCDualβπΎ)βπ))) |
33 | | eqid 2737 |
. . . . . . . . . 10
β’
(Baseβ((LCDualβπΎ)βπ)) = (Baseβ((LCDualβπΎ)βπ)) |
34 | | eqid 2737 |
. . . . . . . . . 10
β’
(Scalarβ((LCDualβπΎ)βπ)) = (Scalarβ((LCDualβπΎ)βπ)) |
35 | | eqid 2737 |
. . . . . . . . . 10
β’
(Baseβ(Scalarβ((LCDualβπΎ)βπ))) =
(Baseβ(Scalarβ((LCDualβπΎ)βπ))) |
36 | | eqid 2737 |
. . . . . . . . . 10
β’
(0gβ(Scalarβ((LCDualβπΎ)βπ))) =
(0gβ(Scalarβ((LCDualβπΎ)βπ))) |
37 | 1, 7, 5 | lcdlvec 40057 |
. . . . . . . . . . 11
β’ (π β ((LCDualβπΎ)βπ) β LVec) |
38 | 37 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β ((LCDualβπΎ)βπ) β LVec) |
39 | 1, 2, 10 | dvhlmod 39576 |
. . . . . . . . . . . 12
β’ ((π β§ π₯ β (Baseβπ)) β π β LMod) |
40 | 39, 26 | syl 17 |
. . . . . . . . . . 11
β’ ((π β§ π₯ β (Baseβπ)) β 0 β (Baseβπ
)) |
41 | 1, 2, 17, 23, 7, 34, 35, 25, 10, 40 | hgmapdcl 40356 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β (πΊβ 0 ) β
(Baseβ(Scalarβ((LCDualβπΎ)βπ)))) |
42 | 1, 2, 3, 7, 33, 9,
10, 11 | hdmapcl 40296 |
. . . . . . . . . 10
β’ ((π β§ π₯ β (Baseβπ)) β (((HDMapβπΎ)βπ)βπ₯) β (Baseβ((LCDualβπΎ)βπ))) |
43 | 33, 24, 34, 35, 36, 8, 38, 41, 42 | lvecvs0or 20572 |
. . . . . . . . 9
β’ ((π β§ π₯ β (Baseβπ)) β (((πΊβ 0 )(
Β·π β((LCDualβπΎ)βπ))(((HDMapβπΎ)βπ)βπ₯)) =
(0gβ((LCDualβπΎ)βπ)) β ((πΊβ 0 ) =
(0gβ(Scalarβ((LCDualβπΎ)βπ))) β¨ (((HDMapβπΎ)βπ)βπ₯) = (0gβ((LCDualβπΎ)βπ))))) |
44 | 32, 43 | mpbid 231 |
. . . . . . . 8
β’ ((π β§ π₯ β (Baseβπ)) β ((πΊβ 0 ) =
(0gβ(Scalarβ((LCDualβπΎ)βπ))) β¨ (((HDMapβπΎ)βπ)βπ₯) = (0gβ((LCDualβπΎ)βπ)))) |
45 | 44 | orcomd 870 |
. . . . . . 7
β’ ((π β§ π₯ β (Baseβπ)) β ((((HDMapβπΎ)βπ)βπ₯) = (0gβ((LCDualβπΎ)βπ)) β¨ (πΊβ 0 ) =
(0gβ(Scalarβ((LCDualβπΎ)βπ))))) |
46 | 45 | ord 863 |
. . . . . 6
β’ ((π β§ π₯ β (Baseβπ)) β (Β¬ (((HDMapβπΎ)βπ)βπ₯) = (0gβ((LCDualβπΎ)βπ)) β (πΊβ 0 ) =
(0gβ(Scalarβ((LCDualβπΎ)βπ))))) |
47 | 46 | 3adant3 1133 |
. . . . 5
β’ ((π β§ π₯ β (Baseβπ) β§ π₯ β (0gβπ)) β (Β¬ (((HDMapβπΎ)βπ)βπ₯) = (0gβ((LCDualβπΎ)βπ)) β (πΊβ 0 ) =
(0gβ(Scalarβ((LCDualβπΎ)βπ))))) |
48 | 15, 47 | mpd 15 |
. . . 4
β’ ((π β§ π₯ β (Baseβπ) β§ π₯ β (0gβπ)) β (πΊβ 0 ) =
(0gβ(Scalarβ((LCDualβπΎ)βπ)))) |
49 | 48 | rexlimdv3a 3157 |
. . 3
β’ (π β (βπ₯ β (Baseβπ)π₯ β (0gβπ) β (πΊβ 0 ) =
(0gβ(Scalarβ((LCDualβπΎ)βπ))))) |
50 | 6, 49 | mpd 15 |
. 2
β’ (π β (πΊβ 0 ) =
(0gβ(Scalarβ((LCDualβπΎ)βπ)))) |
51 | 1, 2, 17, 19, 7, 34, 36, 5 | lcd0 40074 |
. 2
β’ (π β
(0gβ(Scalarβ((LCDualβπΎ)βπ))) = 0 ) |
52 | 50, 51 | eqtrd 2777 |
1
β’ (π β (πΊβ 0 ) = 0 ) |