Metamath Proof Explorer

Theorem hdmap14lem11

Description: Part of proof of part 14 in Baer p. 50 line 3. (Contributed by NM, 3-Jun-2015)

Ref Expression
Hypotheses hdmap14lem8.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmap14lem8.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem8.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmap14lem8.q ⊢ + = ( +g ‘ 𝑈 )
hdmap14lem8.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
hdmap14lem8.o ⊢ 0 = ( 0g ‘ 𝑈 )
hdmap14lem8.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
hdmap14lem8.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hdmap14lem8.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hdmap14lem8.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem8.d ⊢ ✚ = ( +g ‘ 𝐶 )
hdmap14lem8.e ⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
hdmap14lem8.p ⊢ 𝑃 = ( Scalar ‘ 𝐶 )
hdmap14lem8.a ⊢ 𝐴 = ( Base ‘ 𝑃 )
hdmap14lem8.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem8.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmap14lem8.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
hdmap14lem8.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
hdmap14lem8.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
hdmap14lem8.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
hdmap14lem8.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐴 )
hdmap14lem8.xx ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) )
hdmap14lem8.yy ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑌 ) ) = ( 𝐼 ∙ ( 𝑆 ‘ 𝑌 ) ) )
Assertion hdmap14lem11 ( 𝜑 → 𝐺 = 𝐼 )

Proof

Step Hyp Ref Expression
1 hdmap14lem8.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmap14lem8.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmap14lem8.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmap14lem8.q ⊢ + = ( +g ‘ 𝑈 )
5 hdmap14lem8.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
6 hdmap14lem8.o ⊢ 0 = ( 0g ‘ 𝑈 )
7 hdmap14lem8.n ⊢ 𝑁 = ( LSpan ‘ 𝑈 )
8 hdmap14lem8.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
9 hdmap14lem8.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
10 hdmap14lem8.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
11 hdmap14lem8.d ⊢ ✚ = ( +g ‘ 𝐶 )
12 hdmap14lem8.e ⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
13 hdmap14lem8.p ⊢ 𝑃 = ( Scalar ‘ 𝐶 )
14 hdmap14lem8.a ⊢ 𝐴 = ( Base ‘ 𝑃 )
15 hdmap14lem8.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
16 hdmap14lem8.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
17 hdmap14lem8.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
18 hdmap14lem8.y ⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
19 hdmap14lem8.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
20 hdmap14lem8.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
21 hdmap14lem8.i ⊢ ( 𝜑 → 𝐼 ∈ 𝐴 )
22 hdmap14lem8.xx ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) )
23 hdmap14lem8.yy ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑌 ) ) = ( 𝐼 ∙ ( 𝑆 ‘ 𝑌 ) ) )
24 17 eldifad ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
25 18 eldifad ⊢ ( 𝜑 → 𝑌 ∈ 𝑉 )
26 1 2 3 7 16 24 25 dvh3dim ⊢ ( 𝜑 → ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
27 eqid ⊢ ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
28 16 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
29 simp2 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → 𝑧 ∈ 𝑉 )
30 19 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → 𝐹 ∈ 𝐵 )
31 1 2 3 5 8 9 10 12 27 13 14 15 28 29 30 hdmap14lem2a ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) )
32 simp11 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝜑 )
33 32 16 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
34 eqid ⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
35 1 2 16 dvhlmod ⊢ ( 𝜑 → 𝑈 ∈ LMod )
36 32 35 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝑈 ∈ LMod )
37 3 34 7 35 24 25 lspprcl ⊢ ( 𝜑 → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
38 32 37 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ∈ ( LSubSp ‘ 𝑈 ) )
39 simp12 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝑧 ∈ 𝑉 )
40 simp13 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) )
41 6 34 36 38 39 40 lssneln0 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝑧 ∈ ( 𝑉 ∖ { 0 } ) )
42 32 17 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
43 32 19 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝐹 ∈ 𝐵 )
44 simp2 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝑔 ∈ 𝐴 )
45 32 20 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝐺 ∈ 𝐴 )
46 simp3 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) )
47 32 22 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) )
48 1 2 16 dvhlvec ⊢ ( 𝜑 → 𝑈 ∈ LVec )
49 32 48 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝑈 ∈ LVec )
50 32 24 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝑋 ∈ 𝑉 )
51 32 25 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝑌 ∈ 𝑉 )
52 3 7 49 39 50 51 40 lspindpi ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → ( ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) ∧ ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) ) )
53 52 simpld ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { 𝑋 } ) )
54 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 33 41 42 43 44 45 46 47 53 hdmap14lem10 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝑔 = 𝐺 )
55 32 18 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
56 32 21 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝐼 ∈ 𝐴 )
57 32 23 syl ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑌 ) ) = ( 𝐼 ∙ ( 𝑆 ‘ 𝑌 ) ) )
58 52 simprd ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → ( 𝑁 ‘ { 𝑧 } ) ≠ ( 𝑁 ‘ { 𝑌 } ) )
59 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 33 41 55 43 44 56 46 57 58 hdmap14lem10 ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝑔 = 𝐼 )
60 54 59 eqtr3d ⊢ ( ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) ) → 𝐺 = 𝐼 )
61 60 rexlimdv3a ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → ( ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑧 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑧 ) ) → 𝐺 = 𝐼 ) )
62 31 61 mpd ⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝑉 ∧ ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) ) → 𝐺 = 𝐼 )
63 62 rexlimdv3a ⊢ ( 𝜑 → ( ∃ 𝑧 ∈ 𝑉 ¬ 𝑧 ∈ ( 𝑁 ‘ { 𝑋 , 𝑌 } ) → 𝐺 = 𝐼 ) )
64 26 63 mpd ⊢ ( 𝜑 → 𝐺 = 𝐼 )