Metamath Proof Explorer

Theorem hdmap14lem6

Description: Case where F is zero. (Contributed by NM, 1-Jun-2015)

Ref Expression
Hypotheses hdmap14lem1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmap14lem1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmap14lem1.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
hdmap14lem3.o ⊢ 0 = ( 0g ‘ 𝑈 )
hdmap14lem1.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hdmap14lem1.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hdmap14lem1.z ⊢ 𝑍 = ( 0g ‘ 𝑅 )
hdmap14lem1.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem2.e ⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
hdmap14lem1.l ⊢ 𝐿 = ( LSpan ‘ 𝐶 )
hdmap14lem2.p ⊢ 𝑃 = ( Scalar ‘ 𝐶 )
hdmap14lem2.a ⊢ 𝐴 = ( Base ‘ 𝑃 )
hdmap14lem2.q ⊢ 𝑄 = ( 0g ‘ 𝑃 )
hdmap14lem1.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmap14lem3.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
hdmap14lem6.f ⊢ ( 𝜑 → 𝐹 = 𝑍 )
Assertion hdmap14lem6 ( 𝜑 → ∃! 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 hdmap14lem1.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmap14lem1.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmap14lem1.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmap14lem1.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
5 hdmap14lem3.o ⊢ 0 = ( 0g ‘ 𝑈 )
6 hdmap14lem1.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
7 hdmap14lem1.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
8 hdmap14lem1.z ⊢ 𝑍 = ( 0g ‘ 𝑅 )
9 hdmap14lem1.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
10 hdmap14lem2.e ⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
11 hdmap14lem1.l ⊢ 𝐿 = ( LSpan ‘ 𝐶 )
12 hdmap14lem2.p ⊢ 𝑃 = ( Scalar ‘ 𝐶 )
13 hdmap14lem2.a ⊢ 𝐴 = ( Base ‘ 𝑃 )
14 hdmap14lem2.q ⊢ 𝑄 = ( 0g ‘ 𝑃 )
15 hdmap14lem1.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
16 hdmap14lem1.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 hdmap14lem3.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
18 hdmap14lem6.f ⊢ ( 𝜑 → 𝐹 = 𝑍 )
19 1 9 16 lcdlmod ⊢ ( 𝜑 → 𝐶 ∈ LMod )
20 12 13 14 lmod0cl ⊢ ( 𝐶 ∈ LMod → 𝑄 ∈ 𝐴 )
21 19 20 syl ⊢ ( 𝜑 → 𝑄 ∈ 𝐴 )
22 eqid ⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
23 17 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
24 1 2 3 9 22 15 16 23 hdmapcl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝐶 ) )
25 eqid ⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
26 22 12 10 14 25 lmod0vs ⊢ ( ( 𝐶 ∈ LMod ∧ ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝐶 ) ) → ( 𝑄 ∙ ( 𝑆 ‘ 𝑋 ) ) = ( 0g ‘ 𝐶 ) )
27 19 24 26 syl2anc ⊢ ( 𝜑 → ( 𝑄 ∙ ( 𝑆 ‘ 𝑋 ) ) = ( 0g ‘ 𝐶 ) )
28 27 eqcomd ⊢ ( 𝜑 → ( 0g ‘ 𝐶 ) = ( 𝑄 ∙ ( 𝑆 ‘ 𝑋 ) ) )
29 oveq1 ⊢ ( 𝑔 = 𝑄 → ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) = ( 𝑄 ∙ ( 𝑆 ‘ 𝑋 ) ) )
30 29 rspceeqv ⊢ ( ( 𝑄 ∈ 𝐴 ∧ ( 0g ‘ 𝐶 ) = ( 𝑄 ∙ ( 𝑆 ‘ 𝑋 ) ) ) → ∃ 𝑔 ∈ 𝐴 ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) )
31 21 28 30 syl2anc ⊢ ( 𝜑 → ∃ 𝑔 ∈ 𝐴 ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) )
32 1 2 3 5 9 25 22 15 16 17 hdmapnzcl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ∈ ( ( Base ‘ 𝐶 ) ∖ { ( 0g ‘ 𝐶 ) } ) )
33 eldifsni ⊢ ( ( 𝑆 ‘ 𝑋 ) ∈ ( ( Base ‘ 𝐶 ) ∖ { ( 0g ‘ 𝐶 ) } ) → ( 𝑆 ‘ 𝑋 ) ≠ ( 0g ‘ 𝐶 ) )
34 32 33 syl ⊢ ( 𝜑 → ( 𝑆 ‘ 𝑋 ) ≠ ( 0g ‘ 𝐶 ) )
35 34 neneqd ⊢ ( 𝜑 → ¬ ( 𝑆 ‘ 𝑋 ) = ( 0g ‘ 𝐶 ) )
36 35 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ¬ ( 𝑆 ‘ 𝑋 ) = ( 0g ‘ 𝐶 ) )
37 simp3l ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) )
38 37 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) = ( 0g ‘ 𝐶 ) )
39 1 9 16 lcdlvec ⊢ ( 𝜑 → 𝐶 ∈ LVec )
40 39 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → 𝐶 ∈ LVec )
41 simp2l ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → 𝑔 ∈ 𝐴 )
42 24 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( 𝑆 ‘ 𝑋 ) ∈ ( Base ‘ 𝐶 ) )
43 22 10 12 13 14 25 40 41 42 lvecvs0or ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) = ( 0g ‘ 𝐶 ) ↔ ( 𝑔 = 𝑄 ∨ ( 𝑆 ‘ 𝑋 ) = ( 0g ‘ 𝐶 ) ) ) )
44 38 43 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( 𝑔 = 𝑄 ∨ ( 𝑆 ‘ 𝑋 ) = ( 0g ‘ 𝐶 ) ) )
45 44 orcomd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( ( 𝑆 ‘ 𝑋 ) = ( 0g ‘ 𝐶 ) ∨ 𝑔 = 𝑄 ) )
46 45 ord ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( ¬ ( 𝑆 ‘ 𝑋 ) = ( 0g ‘ 𝐶 ) → 𝑔 = 𝑄 ) )
47 36 46 mpd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → 𝑔 = 𝑄 )
48 simp3r ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) )
49 48 eqcomd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) = ( 0g ‘ 𝐶 ) )
50 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ℎ ∈ 𝐴 )
51 22 10 12 13 14 25 40 50 42 lvecvs0or ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) = ( 0g ‘ 𝐶 ) ↔ ( ℎ = 𝑄 ∨ ( 𝑆 ‘ 𝑋 ) = ( 0g ‘ 𝐶 ) ) ) )
52 49 51 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( ℎ = 𝑄 ∨ ( 𝑆 ‘ 𝑋 ) = ( 0g ‘ 𝐶 ) ) )
53 52 orcomd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( ( 𝑆 ‘ 𝑋 ) = ( 0g ‘ 𝐶 ) ∨ ℎ = 𝑄 ) )
54 53 ord ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ( ¬ ( 𝑆 ‘ 𝑋 ) = ( 0g ‘ 𝐶 ) → ℎ = 𝑄 ) )
55 36 54 mpd ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → ℎ = 𝑄 )
56 47 55 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) ∧ ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) ) → 𝑔 = ℎ )
57 56 3exp ⊢ ( 𝜑 → ( ( 𝑔 ∈ 𝐴 ∧ ℎ ∈ 𝐴 ) → ( ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) → 𝑔 = ℎ ) ) )
58 57 ralrimivv ⊢ ( 𝜑 → ∀ 𝑔 ∈ 𝐴 ∀ ℎ ∈ 𝐴 ( ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) → 𝑔 = ℎ ) )
59 oveq1 ⊢ ( 𝑔 = ℎ → ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) )
60 59 eqeq2d ⊢ ( 𝑔 = ℎ → ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ↔ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
61 60 reu4 ⊢ ( ∃! 𝑔 ∈ 𝐴 ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ↔ ( ∃ 𝑔 ∈ 𝐴 ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ∀ 𝑔 ∈ 𝐴 ∀ ℎ ∈ 𝐴 ( ( ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ ( 0g ‘ 𝐶 ) = ( ℎ ∙ ( 𝑆 ‘ 𝑋 ) ) ) → 𝑔 = ℎ ) ) )
62 31 58 61 sylanbrc ⊢ ( 𝜑 → ∃! 𝑔 ∈ 𝐴 ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) )
63 18 oveq1d ⊢ ( 𝜑 → ( 𝐹 · 𝑋 ) = ( 𝑍 · 𝑋 ) )
64 1 2 16 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
65 3 6 4 8 5 lmod0vs ⊢ ( ( 𝑈 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑍 · 𝑋 ) = 0 )
66 64 23 65 syl2anc ⊢ ( 𝜑 → ( 𝑍 · 𝑋 ) = 0 )
67 63 66 eqtrd ⊢ ( 𝜑 → ( 𝐹 · 𝑋 ) = 0 )
68 67 fveq2d ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑆 ‘ 0 ) )
69 1 2 5 9 25 15 16 hdmapval0 ⊢ ( 𝜑 → ( 𝑆 ‘ 0 ) = ( 0g ‘ 𝐶 ) )
70 68 69 eqtrd ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 0g ‘ 𝐶 ) )
71 70 eqeq1d ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ↔ ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
72 71 reubidv ⊢ ( 𝜑 → ( ∃! 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ↔ ∃! 𝑔 ∈ 𝐴 ( 0g ‘ 𝐶 ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
73 62 72 mpbird ⊢ ( 𝜑 → ∃! 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑋 ) ) )