Metamath Proof Explorer

Theorem qusvsval

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 ⊢ ( 𝜑 → 𝐾 ∈ 𝑆 )
qusvsval.n ⊢ 𝑁 = ( 𝑀 /s ( 𝑀 ~QG 𝐺 ) )
qusvsval.m ⊢ ∙ = ( ·𝑠 ‘ 𝑁 )
qusvsval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
Assertion qusvsval ( 𝜑 → ( 𝐾 ∙ [ 𝑋 ] ( 𝑀 ~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 qusvsval.n ⊢ 𝑁 = ( 𝑀 /s ( 𝑀 ~QG 𝐺 ) )
9 qusvsval.m ⊢ ∙ = ( ·𝑠 ‘ 𝑁 )
10 qusvsval.x ⊢ ( 𝜑 → 𝑋 ∈ 𝐵 )
11 8 a1i ⊢ ( 𝜑 → 𝑁 = ( 𝑀 /s ( 𝑀 ~QG 𝐺 ) ) )
12 1 a1i ⊢ ( 𝜑 → 𝐵 = ( Base ‘ 𝑀 ) )
13 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) )
14 ovex ⊢ ( 𝑀 ~QG 𝐺 ) ∈ V
15 14 a1i ⊢ ( 𝜑 → ( 𝑀 ~QG 𝐺 ) ∈ V )
16 11 12 13 15 5 qusval ⊢ ( 𝜑 → 𝑁 = ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) “s 𝑀 ) )
17 11 12 13 15 5 quslem ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) : 𝐵 –onto→ ( 𝐵 / ( 𝑀 ~QG 𝐺 ) ) )
18 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
19 5 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑀 ∈ LMod )
20 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → 𝐺 ∈ ( LSubSp ‘ 𝑀 ) )
21 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑘 ∈ 𝑆 )
22 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑢 ∈ 𝐵 )
23 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → 𝑣 ∈ 𝐵 )
24 1 2 3 4 19 20 21 8 9 13 22 23 qusvscpbl ⊢ ( ( 𝜑 ∧ ( 𝑘 ∈ 𝑆 ∧ 𝑢 ∈ 𝐵 ∧ 𝑣 ∈ 𝐵 ) ) → ( ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑢 ) = ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑣 ) → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝑘 · 𝑢 ) ) = ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝑘 · 𝑣 ) ) ) )
25 16 12 17 5 18 3 4 9 24 imasvscaval ⊢ ( ( 𝜑 ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 ∙ ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑋 ) ) = ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝐾 · 𝑋 ) ) )
26 7 10 25 mpd3an23 ⊢ ( 𝜑 → ( 𝐾 ∙ ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑋 ) ) = ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝐾 · 𝑋 ) ) )
27 eceq1 ⊢ ( 𝑥 = 𝑋 → [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) = [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) )
28 ecexg ⊢ ( ( 𝑀 ~QG 𝐺 ) ∈ V → [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) ∈ V )
29 14 28 ax-mp ⊢ [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) ∈ V
30 27 13 29 fvmpt ⊢ ( 𝑋 ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑋 ) = [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) )
31 10 30 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑋 ) = [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) )
32 31 oveq2d ⊢ ( 𝜑 → ( 𝐾 ∙ ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ 𝑋 ) ) = ( 𝐾 ∙ [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) ) )
33 1 18 4 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 · 𝑋 ) ∈ 𝐵 )
34 5 7 10 33 syl3anc ⊢ ( 𝜑 → ( 𝐾 · 𝑋 ) ∈ 𝐵 )
35 eceq1 ⊢ ( 𝑥 = ( 𝐾 · 𝑋 ) → [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) = [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) )
36 ecexg ⊢ ( ( 𝑀 ~QG 𝐺 ) ∈ V → [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) ∈ V )
37 14 36 ax-mp ⊢ [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) ∈ V
38 35 13 37 fvmpt ⊢ ( ( 𝐾 · 𝑋 ) ∈ 𝐵 → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝐾 · 𝑋 ) ) = [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) )
39 34 38 syl ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) ) ‘ ( 𝐾 · 𝑋 ) ) = [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) )
40 26 32 39 3eqtr3d ⊢ ( 𝜑 → ( 𝐾 ∙ [ 𝑋 ] ( 𝑀 ~QG 𝐺 ) ) = [ ( 𝐾 · 𝑋 ) ] ( 𝑀 ~QG 𝐺 ) )