Metamath Proof Explorer

Theorem qusscaval

Description: Value of the scalar multiplication operation on the quotient structure. (Contributed by Thierry Arnoux, 18-May-2023)

Ref Expression
Hypotheses eqgvscpbl.v ⊢ 𝐵 = ( Base ‘ 𝑀 )
eqgvscpbl.e ⊢ ∼ = ( 𝑀 ~QG 𝐺 )
eqgvscpbl.s ⊢ 𝑆 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
eqgvscpbl.p ⊢ · = ( ·𝑠 ‘ 𝑀 )
eqgvscpbl.m ⊢ ( 𝜑 → 𝑀 ∈ LMod )
eqgvscpbl.g ⊢ ( 𝜑 → 𝐺 ∈ ( LSubSp ‘ 𝑀 ) )
eqgvscpbl.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑆 )
qusscaval.n ⊢ 𝑁 = ( 𝑀 /s ( 𝑀 ~QG 𝐺 ) )
qusscaval.m ⊢ ∙ = ( ·𝑠 ‘ 𝑁 )
Assertion qusscaval ( ( 𝜑 ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 ∙ [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) ) = [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) )

Proof

Step Hyp Ref Expression
1 eqgvscpbl.v ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 eqgvscpbl.e ⊢ ∼ = ( 𝑀 ~QG 𝐺 )
3 eqgvscpbl.s ⊢ 𝑆 = ( Base ‘ ( Scalar ‘ 𝑀 ) )
4 eqgvscpbl.p ⊢ · = ( ·𝑠 ‘ 𝑀 )
5 eqgvscpbl.m ⊢ ( 𝜑 → 𝑀 ∈ LMod )
6 eqgvscpbl.g ⊢ ( 𝜑 → 𝐺 ∈ ( LSubSp ‘ 𝑀 ) )
7 eqgvscpbl.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑆 )
8 qusscaval.n ⊢ 𝑁 = ( 𝑀 /s ( 𝑀 ~QG 𝐺 ) )
9 qusscaval.m ⊢ ∙ = ( ·𝑠 ‘ 𝑁 )
10 8 a1i ⊢ ( 𝜑 → 𝑁 = ( 𝑀 /s ( 𝑀 ~QG 𝐺 ) ) )
11 1 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑀 ) )
12 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) )
13 ovex ⊢ ( 𝑀 ~QG 𝐺 ) ∈ V
14 13 a1i ⊢ ( 𝜑 → ( 𝑀 ~QG 𝐺 ) ∈ V )
15 10 11 12 14 5 qusval ⊢ ( 𝜑 → 𝑁 = ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) “s 𝑀 ) )
16 10 11 12 14 5 quslem ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) : 𝐵 –onto→ ( 𝐵 / ( 𝑀 ~QG 𝐺 ) ) )
17 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
18 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑀 ∈ LMod )
19 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → 𝐺 ∈ ( LSubSp ‘ 𝑀 ) )
20 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑘 ∈ 𝑆 )
21 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑢 ∈ 𝐵 )
22 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑣 ∈ 𝐵 )
23 1 2 3 4 18 19 20 8 9 12 21 22 qusvscpbl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑣 ) → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝑘 · 𝑢 ) ) = ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝑘 · 𝑣 ) ) ) )
24 15 11 16 5 17 3 4 9 23 imasvscaval ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 ∙ ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑋 ) ) = ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝐾 · 𝑋 ) ) )
25 eceq1 ⊢ ( 𝑥 = 𝑋 → [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) = [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) )
26 ecexg ⊢ ( ( 𝑀 ~QG 𝐺 ) ∈ V → [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) ∈ V )
27 13 26 ax-mp ⊢ [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) ∈ V
28 25 12 27 fvmpt ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑋 ) = [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) )
29 28 3ad2ant3 ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑋 ) = [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) )
30 29 oveq2d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 ∙ ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑋 ) ) = ( 𝐾 ∙ [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) ) )
31 1 17 4 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 · 𝑋 ) ∈ 𝐵 )
32 5 31 syl3an1 ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 · 𝑋 ) ∈ 𝐵 )
33 eceq1 ⊢ ( 𝑥 = ( 𝐾 · 𝑋 ) → [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) = [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) )
34 ecexg ⊢ ( ( 𝑀 ~QG 𝐺 ) ∈ V → [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) ∈ V )
35 13 34 ax-mp ⊢ [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) ∈ V
36 33 12 35 fvmpt ⊢ ( ( 𝐾 · 𝑋 ) ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝐾 · 𝑋 ) ) = [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) )
37 32 36 syl ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝐾 · 𝑋 ) ) = [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) )
38 24 30 37 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 ∙ [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) ) = [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) )