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 ⊢ H = LHyp ⁡ K
hgmapval0.u ⊢ U = DVecH ⁡ K ⁡ W
hgmapval0.r ⊢ R = Scalar ⁡ U
hgmapval0.o ⊢ 0 ˙ = 0 R
hgmapval0.g ⊢ G = HGMap ⁡ K ⁡ W
hgmapval0.k ⊢ φ → K ∈ HL ∧ W ∈ H
Assertion hgmapval0 ⊢ φ → G ⁡ 0 ˙ = 0 ˙

Proof

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