Metamath Proof Explorer

Theorem hdmap14lem12

Description: Lemma for proof of part 14 in Baer p. 50. (Contributed by NM, 6-Jun-2015)

Ref Expression
Hypotheses hdmap14lem12.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hdmap14lem12.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem12.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hdmap14lem12.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
hdmap14lem12.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hdmap14lem12.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hdmap14lem12.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem12.e ⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
hdmap14lem12.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hdmap14lem12.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hdmap14lem12.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
hdmap14lem12.p ⊢ 𝑃 = ( Scalar ‘ 𝐶 )
hdmap14lem12.a ⊢ 𝐴 = ( Base ‘ 𝑃 )
hdmap14lem12.o ⊢ 0 = ( 0g ‘ 𝑈 )
hdmap14lem12.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
hdmap14lem12.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
Assertion hdmap14lem12 ( 𝜑 → ( ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ↔ ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 hdmap14lem12.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hdmap14lem12.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hdmap14lem12.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hdmap14lem12.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
5 hdmap14lem12.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6 hdmap14lem12.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
7 hdmap14lem12.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
8 hdmap14lem12.e ⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
9 hdmap14lem12.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
10 hdmap14lem12.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
11 hdmap14lem12.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
12 hdmap14lem12.p ⊢ 𝑃 = ( Scalar ‘ 𝐶 )
13 hdmap14lem12.a ⊢ 𝐴 = ( Base ‘ 𝑃 )
14 hdmap14lem12.o ⊢ 0 = ( 0g ‘ 𝑈 )
15 hdmap14lem12.x ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
16 hdmap14lem12.g ⊢ ( 𝜑 → 𝐺 ∈ 𝐴 )
17 eqid ⊢ ( LSpan ‘ 𝐶 ) = ( LSpan ‘ 𝐶 )
18 10 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
19 simp3 ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑦 ∈ ( 𝑉 ∖ { 0 } ) )
20 19 eldifad ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝑦 ∈ 𝑉 )
21 11 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → 𝐹 ∈ 𝐵 )
22 1 2 3 4 5 6 7 8 17 12 13 9 18 20 21 hdmap14lem2a ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) )
23 simp3 ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) )
24 eqid ⊢ ( +g ‘ 𝑈 ) = ( +g ‘ 𝑈 )
25 eqid ⊢ ( LSpan ‘ 𝑈 ) = ( LSpan ‘ 𝑈 )
26 eqid ⊢ ( +g ‘ 𝐶 ) = ( +g ‘ 𝐶 )
27 simp11 ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝜑 )
28 27 10 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
29 27 15 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝑋 ∈ ( 𝑉 ∖ { 0 } ) )
30 simp13 ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝑦 ∈ ( 𝑉 ∖ { 0 } ) )
31 27 11 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝐹 ∈ 𝐵 )
32 27 16 syl ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝐺 ∈ 𝐴 )
33 simp2 ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝑔 ∈ 𝐴 )
34 simp12 ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) )
35 1 2 3 24 4 14 25 5 6 7 26 8 12 13 9 28 29 30 31 32 33 34 23 hdmap14lem11 ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → 𝐺 = 𝑔 )
36 35 oveq1d ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) )
37 23 36 eqtr4d ⊢ ( ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) ∧ 𝑔 ∈ 𝐴 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) )
38 37 rexlimdv3a ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → ( ∃ 𝑔 ∈ 𝐴 ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑦 ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) ) )
39 22 38 mpd ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ∧ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) )
40 39 3expia ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ) → ( 𝑦 ∈ ( 𝑉 ∖ { 0 } ) → ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) ) )
41 40 ralrimiv ⊢ ( ( 𝜑 ∧ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ) → ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) )
42 oveq2 ⊢ ( 𝑦 = 𝑋 → ( 𝐹 · 𝑦 ) = ( 𝐹 · 𝑋 ) )
43 42 fveq2d ⊢ ( 𝑦 = 𝑋 → ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) )
44 fveq2 ⊢ ( 𝑦 = 𝑋 → ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑋 ) )
45 44 oveq2d ⊢ ( 𝑦 = 𝑋 → ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) )
46 43 45 eqeq12d ⊢ ( 𝑦 = 𝑋 → ( ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
47 46 rspcv ⊢ ( 𝑋 ∈ ( 𝑉 ∖ { 0 } ) → ( ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
48 15 47 syl ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
49 48 imp ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) )
50 41 49 impbida ⊢ ( 𝜑 → ( ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑋 ) ) ↔ ∀ 𝑦 ∈ ( 𝑉 ∖ { 0 } ) ( 𝑆 ‘ ( 𝐹 · 𝑦 ) ) = ( 𝐺 ∙ ( 𝑆 ‘ 𝑦 ) ) ) )