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 𝐺 ) )