Metamath Proof Explorer

Theorem qusvscpbl

Description: The quotient map distributes over the scalar multiplication. (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 ⊢ ∙ = ( ·𝑠 ‘ 𝑁 )
qusvscpbl.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) )
qusvscpbl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
qusvscpbl.v ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
Assertion qusvscpbl ( 𝜑 → ( ( 𝐹 ‘ 𝑈 ) = ( 𝐹 ‘ 𝑉 ) → ( 𝐹 ‘ ( 𝐾 · 𝑈 ) ) = ( 𝐹 ‘ ( 𝐾 · 𝑉 ) ) ) )

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 qusvscpbl.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) )
11 qusvscpbl.u ⊢ ( 𝜑 → 𝑈 ∈ 𝐵 )
12 qusvscpbl.v ⊢ ( 𝜑 → 𝑉 ∈ 𝐵 )
13 eqid ⊢ ( 𝑀 ~QG 𝐺 ) = ( 𝑀 ~QG 𝐺 )
14 1 13 3 4 5 6 7 eqgvscpbl ⊢ ( 𝜑 → ( 𝑈 ( 𝑀 ~QG 𝐺 ) 𝑉 → ( 𝐾 · 𝑈 ) ( 𝑀 ~QG 𝐺 ) ( 𝐾 · 𝑉 ) ) )
15 eqid ⊢ ( LSubSp ‘ 𝑀 ) = ( LSubSp ‘ 𝑀 )
16 15 lsssubg ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐺 ∈ ( LSubSp ‘ 𝑀 ) ) → 𝐺 ∈ ( SubGrp ‘ 𝑀 ) )
17 5 6 16 syl2anc ⊢ ( 𝜑 → 𝐺 ∈ ( SubGrp ‘ 𝑀 ) )
18 1 13 eqger ⊢ ( 𝐺 ∈ ( SubGrp ‘ 𝑀 ) → ( 𝑀 ~QG 𝐺 ) Er 𝐵 )
19 17 18 syl ⊢ ( 𝜑 → ( 𝑀 ~QG 𝐺 ) Er 𝐵 )
20 19 11 erth ⊢ ( 𝜑 → ( 𝑈 ( 𝑀 ~QG 𝐺 ) 𝑉 ↔ [ 𝑈 ] ( 𝑀 ~QG 𝐺 ) = [ 𝑉 ] ( 𝑀 ~QG 𝐺 ) ) )
21 eqid ⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
22 1 21 4 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐾 ∈ 𝑆 ∧ 𝑈 ∈ 𝐵 ) → ( 𝐾 · 𝑈 ) ∈ 𝐵 )
23 5 7 11 22 syl3anc ⊢ ( 𝜑 → ( 𝐾 · 𝑈 ) ∈ 𝐵 )
24 19 23 erth ⊢ ( 𝜑 → ( ( 𝐾 · 𝑈 ) ( 𝑀 ~QG 𝐺 ) ( 𝐾 · 𝑉 ) ↔ [ ( 𝐾 · 𝑈 ) ] ( 𝑀 ~QG 𝐺 ) = [ ( 𝐾 · 𝑉 ) ] ( 𝑀 ~QG 𝐺 ) ) )
25 14 20 24 3imtr3d ⊢ ( 𝜑 → ( [ 𝑈 ] ( 𝑀 ~QG 𝐺 ) = [ 𝑉 ] ( 𝑀 ~QG 𝐺 ) → [ ( 𝐾 · 𝑈 ) ] ( 𝑀 ~QG 𝐺 ) = [ ( 𝐾 · 𝑉 ) ] ( 𝑀 ~QG 𝐺 ) ) )
26 eceq1 ⊢ ( 𝑥 = 𝑈 → [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) = [ 𝑈 ] ( 𝑀 ~QG 𝐺 ) )
27 ovex ⊢ ( 𝑀 ~QG 𝐺 ) ∈ V
28 ecexg ⊢ ( ( 𝑀 ~QG 𝐺 ) ∈ V → [ 𝑈 ] ( 𝑀 ~QG 𝐺 ) ∈ V )
29 27 28 ax-mp ⊢ [ 𝑈 ] ( 𝑀 ~QG 𝐺 ) ∈ V
30 26 10 29 fvmpt ⊢ ( 𝑈 ∈ 𝐵 → ( 𝐹 ‘ 𝑈 ) = [ 𝑈 ] ( 𝑀 ~QG 𝐺 ) )
31 11 30 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑈 ) = [ 𝑈 ] ( 𝑀 ~QG 𝐺 ) )
32 eceq1 ⊢ ( 𝑥 = 𝑉 → [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) = [ 𝑉 ] ( 𝑀 ~QG 𝐺 ) )
33 ecexg ⊢ ( ( 𝑀 ~QG 𝐺 ) ∈ V → [ 𝑉 ] ( 𝑀 ~QG 𝐺 ) ∈ V )
34 27 33 ax-mp ⊢ [ 𝑉 ] ( 𝑀 ~QG 𝐺 ) ∈ V
35 32 10 34 fvmpt ⊢ ( 𝑉 ∈ 𝐵 → ( 𝐹 ‘ 𝑉 ) = [ 𝑉 ] ( 𝑀 ~QG 𝐺 ) )
36 12 35 syl ⊢ ( 𝜑 → ( 𝐹 ‘ 𝑉 ) = [ 𝑉 ] ( 𝑀 ~QG 𝐺 ) )
37 31 36 eqeq12d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑈 ) = ( 𝐹 ‘ 𝑉 ) ↔ [ 𝑈 ] ( 𝑀 ~QG 𝐺 ) = [ 𝑉 ] ( 𝑀 ~QG 𝐺 ) ) )
38 eceq1 ⊢ ( 𝑥 = ( 𝐾 · 𝑈 ) → [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) = [ ( 𝐾 · 𝑈 ) ] ( 𝑀 ~QG 𝐺 ) )
39 ecexg ⊢ ( ( 𝑀 ~QG 𝐺 ) ∈ V → [ ( 𝐾 · 𝑈 ) ] ( 𝑀 ~QG 𝐺 ) ∈ V )
40 27 39 ax-mp ⊢ [ ( 𝐾 · 𝑈 ) ] ( 𝑀 ~QG 𝐺 ) ∈ V
41 38 10 40 fvmpt ⊢ ( ( 𝐾 · 𝑈 ) ∈ 𝐵 → ( 𝐹 ‘ ( 𝐾 · 𝑈 ) ) = [ ( 𝐾 · 𝑈 ) ] ( 𝑀 ~QG 𝐺 ) )
42 23 41 syl ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐾 · 𝑈 ) ) = [ ( 𝐾 · 𝑈 ) ] ( 𝑀 ~QG 𝐺 ) )
43 1 21 4 3 lmodvscl ⊢ ( ( 𝑀 ∈ LMod ∧ 𝐾 ∈ 𝑆 ∧ 𝑉 ∈ 𝐵 ) → ( 𝐾 · 𝑉 ) ∈ 𝐵 )
44 5 7 12 43 syl3anc ⊢ ( 𝜑 → ( 𝐾 · 𝑉 ) ∈ 𝐵 )
45 eceq1 ⊢ ( 𝑥 = ( 𝐾 · 𝑉 ) → [ 𝑥 ] ( 𝑀 ~QG 𝐺 ) = [ ( 𝐾 · 𝑉 ) ] ( 𝑀 ~QG 𝐺 ) )
46 ecexg ⊢ ( ( 𝑀 ~QG 𝐺 ) ∈ V → [ ( 𝐾 · 𝑉 ) ] ( 𝑀 ~QG 𝐺 ) ∈ V )
47 27 46 ax-mp ⊢ [ ( 𝐾 · 𝑉 ) ] ( 𝑀 ~QG 𝐺 ) ∈ V
48 45 10 47 fvmpt ⊢ ( ( 𝐾 · 𝑉 ) ∈ 𝐵 → ( 𝐹 ‘ ( 𝐾 · 𝑉 ) ) = [ ( 𝐾 · 𝑉 ) ] ( 𝑀 ~QG 𝐺 ) )
49 44 48 syl ⊢ ( 𝜑 → ( 𝐹 ‘ ( 𝐾 · 𝑉 ) ) = [ ( 𝐾 · 𝑉 ) ] ( 𝑀 ~QG 𝐺 ) )
50 42 49 eqeq12d ⊢ ( 𝜑 → ( ( 𝐹 ‘ ( 𝐾 · 𝑈 ) ) = ( 𝐹 ‘ ( 𝐾 · 𝑉 ) ) ↔ [ ( 𝐾 · 𝑈 ) ] ( 𝑀 ~QG 𝐺 ) = [ ( 𝐾 · 𝑉 ) ] ( 𝑀 ~QG 𝐺 ) ) )
51 25 37 50 3imtr4d ⊢ ( 𝜑 → ( ( 𝐹 ‘ 𝑈 ) = ( 𝐹 ‘ 𝑉 ) → ( 𝐹 ‘ ( 𝐾 · 𝑈 ) ) = ( 𝐹 ‘ ( 𝐾 · 𝑉 ) ) ) )