Metamath Proof Explorer

Theorem hgmapval0

Description: Value of the scalar sigma map at zero. (Contributed by NM, 12-Jun-2015)

Ref Expression
Hypotheses hgmapval0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hgmapval0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hgmapval0.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hgmapval0.o ⊢ 0 = ( 0g ‘ 𝑅 )
hgmapval0.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hgmapval0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
Assertion hgmapval0 ( 𝜑 → ( 𝐺 ‘ 0 ) = 0 )

Proof

Step Hyp Ref Expression
1 hgmapval0.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hgmapval0.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hgmapval0.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
4 hgmapval0.o ⊢ 0 = ( 0g ‘ 𝑅 )
5 hgmapval0.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
6 hgmapval0.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
7 eqid ⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
8 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
9 1 2 7 8 6 dvh1dim ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Base ‘ 𝑈 ) 𝑥 ≠ ( 0g ‘ 𝑈 ) )
10 eqid ⊢ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
11 eqid ⊢ ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
12 eqid ⊢ ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
13 6 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
14 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → 𝑥 ∈ ( Base ‘ 𝑈 ) )
15 1 2 7 8 10 11 12 13 14 hdmapeq0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ 𝑥 = ( 0g ‘ 𝑈 ) ) )
16 15 biimpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) → 𝑥 = ( 0g ‘ 𝑈 ) ) )
17 16 necon3ad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( 𝑥 ≠ ( 0g ‘ 𝑈 ) → ¬ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
18 17 3impia ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑈 ) ) → ¬ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
19 1 2 6 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
20 eqid ⊢ ( ·𝑠 ‘ 𝑈 ) = ( ·𝑠 ‘ 𝑈 )
21 7 3 20 4 8 lmod0vs ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( 0 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) = ( 0g ‘ 𝑈 ) )
22 19 21 sylan ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( 0 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) = ( 0g ‘ 𝑈 ) )
23 22 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) ) = ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0g ‘ 𝑈 ) ) )
24 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
25 eqid ⊢ ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
26 3 24 4 lmod0cl ⊢ ( 𝑈 ∈ LMod → 0 ∈ ( Base ‘ 𝑅 ) )
27 19 26 syl ⊢ ( 𝜑 → 0 ∈ ( Base ‘ 𝑅 ) )
28 27 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → 0 ∈ ( Base ‘ 𝑅 ) )
29 1 2 7 20 3 24 10 25 12 5 13 14 28 hgmapvs ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0 ( ·𝑠 ‘ 𝑈 ) 𝑥 ) ) = ( ( 𝐺 ‘ 0 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) )
30 1 2 8 10 11 12 6 hdmapval0 ⊢ ( 𝜑 → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0g ‘ 𝑈 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ ( 0g ‘ 𝑈 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
32 23 29 31 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( 𝐺 ‘ 0 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
33 eqid ⊢ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
34 eqid ⊢ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) = ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) )
35 eqid ⊢ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
36 eqid ⊢ ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
37 1 10 6 lcdlvec ⊢ ( 𝜑 → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LVec )
38 37 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ∈ LVec )
39 1 2 13 dvhlmod ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → 𝑈 ∈ LMod )
40 39 26 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → 0 ∈ ( Base ‘ 𝑅 ) )
41 1 2 3 24 10 34 35 5 13 40 hgmapdcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( 𝐺 ‘ 0 ) ∈ ( Base ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
42 1 2 7 10 33 12 13 14 hdmapcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ∈ ( Base ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) )
43 33 25 34 35 36 11 38 41 42 lvecvs0or ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( 𝐺 ‘ 0 ) ( ·𝑠 ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ↔ ( ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∨ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
44 32 43 mpbid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ∨ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
45 44 orcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ∨ ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
46 45 ord ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ) → ( ¬ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
47 46 3adant3 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑈 ) ) → ( ¬ ( ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 ) ‘ 𝑥 ) = ( 0g ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) → ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
48 18 47 mpd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( Base ‘ 𝑈 ) ∧ 𝑥 ≠ ( 0g ‘ 𝑈 ) ) → ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
49 48 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ ( Base ‘ 𝑈 ) 𝑥 ≠ ( 0g ‘ 𝑈 ) → ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) ) )
50 9 49 mpd ⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) )
51 1 2 3 4 10 34 36 6 lcd0 ⊢ ( 𝜑 → ( 0g ‘ ( Scalar ‘ ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 ) ) ) = 0 )
52 50 51 eqtrd ⊢ ( 𝜑 → ( 𝐺 ‘ 0 ) = 0 )