Metamath Proof Explorer

Theorem hgmapvs

Description: Part 15 of Baer p. 50 line 6. Also line 15 in Holland95 p. 14. (Contributed by NM, 6-Jun-2015)

Ref Expression
Hypotheses hgmapvs.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
hgmapvs.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
hgmapvs.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
hgmapvs.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
hgmapvs.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
hgmapvs.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
hgmapvs.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
hgmapvs.e ⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
hgmapvs.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
hgmapvs.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
hgmapvs.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
hgmapvs.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
hgmapvs.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion hgmapvs ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 hgmapvs.h ⊢ 𝐻 = ( LHyp ‘ 𝐾 )
2 hgmapvs.u ⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
3 hgmapvs.v ⊢ 𝑉 = ( Base ‘ 𝑈 )
4 hgmapvs.t ⊢ · = ( ·𝑠 ‘ 𝑈 )
5 hgmapvs.r ⊢ 𝑅 = ( Scalar ‘ 𝑈 )
6 hgmapvs.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
7 hgmapvs.c ⊢ 𝐶 = ( ( LCDual ‘ 𝐾 ) ‘ 𝑊 )
8 hgmapvs.e ⊢ ∙ = ( ·𝑠 ‘ 𝐶 )
9 hgmapvs.s ⊢ 𝑆 = ( ( HDMap ‘ 𝐾 ) ‘ 𝑊 )
10 hgmapvs.g ⊢ 𝐺 = ( ( HGMap ‘ 𝐾 ) ‘ 𝑊 )
11 hgmapvs.k ⊢ ( 𝜑 → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
12 hgmapvs.x ⊢ ( 𝜑 → 𝑋 ∈ 𝑉 )
13 hgmapvs.f ⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
14 1 2 3 4 5 6 7 8 9 10 11 13 hgmapval ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐹 ) = ( ℩ 𝑔 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) )
15 14 eqcomd ⊢ ( 𝜑 → ( ℩ 𝑔 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) = ( 𝐺 ‘ 𝐹 ) )
16 1 2 5 6 10 11 13 hgmapcl ⊢ ( 𝜑 → ( 𝐺 ‘ 𝐹 ) ∈ 𝐵 )
17 1 2 3 4 5 6 7 8 9 11 13 hdmap14lem15 ⊢ ( 𝜑 → ∃! 𝑔 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) )
18 oveq1 ⊢ ( 𝑔 = ( 𝐺 ‘ 𝐹 ) → ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) )
19 18 eqeq2d ⊢ ( 𝑔 = ( 𝐺 ‘ 𝐹 ) → ( ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ↔ ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) ) )
20 19 ralbidv ⊢ ( 𝑔 = ( 𝐺 ‘ 𝐹 ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ↔ ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) ) )
21 20 riota2 ⊢ ( ( ( 𝐺 ‘ 𝐹 ) ∈ 𝐵 ∧ ∃! 𝑔 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) → ( ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) ↔ ( ℩ 𝑔 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) = ( 𝐺 ‘ 𝐹 ) ) )
22 16 17 21 syl2anc ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) ↔ ( ℩ 𝑔 ∈ 𝐵 ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑔 ∙ ( 𝑆 ‘ 𝑥 ) ) ) = ( 𝐺 ‘ 𝐹 ) ) )
23 15 22 mpbird ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) )
24 oveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐹 · 𝑥 ) = ( 𝐹 · 𝑋 ) )
25 24 fveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) )
26 fveq2 ⊢ ( 𝑥 = 𝑋 → ( 𝑆 ‘ 𝑥 ) = ( 𝑆 ‘ 𝑋 ) )
27 26 oveq2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑋 ) ) )
28 25 27 eqeq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) ↔ ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑋 ) ) ) )
29 28 rspcva ⊢ ( ( 𝑋 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝑉 ( 𝑆 ‘ ( 𝐹 · 𝑥 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑥 ) ) ) → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑋 ) ) )
30 12 23 29 syl2anc ⊢ ( 𝜑 → ( 𝑆 ‘ ( 𝐹 · 𝑋 ) ) = ( ( 𝐺 ‘ 𝐹 ) ∙ ( 𝑆 ‘ 𝑋 ) ) )