Theorem eqgvscpbl

Description: The left coset equivalence relation is compatible with the scalar multiplication operation. (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	⊢ ( 𝜑 → 𝐾 ∈ 𝑆 )
Assertion	eqgvscpbl	⊢ ( 𝜑 → ( 𝑋 ∼ 𝑌 → ( 𝐾 · 𝑋 ) ∼ ( 𝐾 · 𝑌 ) ) )

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	5	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → 𝑀 ∈ LMod )
9	7	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → 𝐾 ∈ 𝑆 )
10		simpr1	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → 𝑋 ∈ 𝐵 )
11		eqid	⊢ ( Scalar ‘ 𝑀 ) = ( Scalar ‘ 𝑀 )
12	1 11 4 3	lmodvscl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 · 𝑋 ) ∈ 𝐵 )
13	8 9 10 12	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( 𝐾 · 𝑋 ) ∈ 𝐵 )
14		simpr2	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → 𝑌 ∈ 𝐵 )
15	1 11 4 3	lmodvscl	⊢ ( ( 𝑀 ∈ LMod ∧ 𝐾 ∈ 𝑆 ∧ 𝑌 ∈ 𝐵 ) → ( 𝐾 · 𝑌 ) ∈ 𝐵 )
16	8 9 14 15	syl3anc	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( 𝐾 · 𝑌 ) ∈ 𝐵 )
17	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑌 ∈ 𝐵 ) → 𝑀 ∈ LMod )
18	7	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑌 ∈ 𝐵 ) → 𝐾 ∈ 𝑆 )
19		lmodgrp	⊢ ( 𝑀 ∈ LMod → 𝑀 ∈ Grp )
20	17 19	syl	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑌 ∈ 𝐵 ) → 𝑀 ∈ Grp )
21		simplr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑌 ∈ 𝐵 ) → 𝑋 ∈ 𝐵 )
22		eqid	⊢ ( invg ‘ 𝑀 ) = ( invg ‘ 𝑀 )
23	1 22	grpinvcl	⊢ ( ( 𝑀 ∈ Grp ∧ 𝑋 ∈ 𝐵 ) → ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ∈ 𝐵 )
24	20 21 23	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑌 ∈ 𝐵 ) → ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ∈ 𝐵 )
25		simpr	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑌 ∈ 𝐵 ) → 𝑌 ∈ 𝐵 )
26		eqid	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
27	1 26 11 4 3	lmodvsdi	⊢ ( ( 𝑀 ∈ LMod ∧ ( 𝐾 ∈ 𝑆 ∧ ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐾 · ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ) = ( ( 𝐾 · ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝐾 · 𝑌 ) ) )
28	17 18 24 25 27	syl13anc	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝐾 · ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ) = ( ( 𝐾 · ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝐾 · 𝑌 ) ) )
29	1 11 4 22 3	lmodvsinv2	⊢ ( ( 𝑀 ∈ LMod ∧ 𝐾 ∈ 𝑆 ∧ 𝑋 ∈ 𝐵 ) → ( 𝐾 · ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ) = ( ( invg ‘ 𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) )
30	17 18 21 29	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝐾 · ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ) = ( ( invg ‘ 𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) )
31	30	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝐾 · ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝐾 · 𝑌 ) ) = ( ( ( invg ‘ 𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝐾 · 𝑌 ) ) )
32	28 31	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑋 ∈ 𝐵 ) ∧ 𝑌 ∈ 𝐵 ) → ( 𝐾 · ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ) = ( ( ( invg ‘ 𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝐾 · 𝑌 ) ) )
33	32	anasss	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) ) → ( 𝐾 · ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ) = ( ( ( invg ‘ 𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝐾 · 𝑌 ) ) )
34	33	3adantr3	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( 𝐾 · ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ) = ( ( ( invg ‘ 𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝐾 · 𝑌 ) ) )
35	6	adantr	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → 𝐺 ∈ ( LSubSp ‘ 𝑀 ) )
36		simpr3	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 )
37		eqid	⊢ ( LSubSp ‘ 𝑀 ) = ( LSubSp ‘ 𝑀 )
38	11 4 3 37	lssvscl	⊢ ( ( ( 𝑀 ∈ LMod ∧ 𝐺 ∈ ( LSubSp ‘ 𝑀 ) ) ∧ ( 𝐾 ∈ 𝑆 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( 𝐾 · ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ) ∈ 𝐺 )
39	8 35 9 36 38	syl22anc	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( 𝐾 · ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ) ∈ 𝐺 )
40	34 39	eqeltrrd	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( ( ( invg ‘ 𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝐾 · 𝑌 ) ) ∈ 𝐺 )
41	13 16 40	3jca	⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) → ( ( 𝐾 · 𝑋 ) ∈ 𝐵 ∧ ( 𝐾 · 𝑌 ) ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝐾 · 𝑌 ) ) ∈ 𝐺 ) )
42	41	ex	⊢ ( 𝜑 → ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) → ( ( 𝐾 · 𝑋 ) ∈ 𝐵 ∧ ( 𝐾 · 𝑌 ) ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝐾 · 𝑌 ) ) ∈ 𝐺 ) ) )
43	5 19	syl	⊢ ( 𝜑 → 𝑀 ∈ Grp )
44	37	lsssubg	⊢ ( ( 𝑀 ∈ LMod ∧ 𝐺 ∈ ( LSubSp ‘ 𝑀 ) ) → 𝐺 ∈ ( SubGrp ‘ 𝑀 ) )
45	5 6 44	syl2anc	⊢ ( 𝜑 → 𝐺 ∈ ( SubGrp ‘ 𝑀 ) )
46	1	subgss	⊢ ( 𝐺 ∈ ( SubGrp ‘ 𝑀 ) → 𝐺 ⊆ 𝐵 )
47	45 46	syl	⊢ ( 𝜑 → 𝐺 ⊆ 𝐵 )
48	1 22 26 2	eqgval	⊢ ( ( 𝑀 ∈ Grp ∧ 𝐺 ⊆ 𝐵 ) → ( 𝑋 ∼ 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) )
49	43 47 48	syl2anc	⊢ ( 𝜑 → ( 𝑋 ∼ 𝑌 ↔ ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑋 ) ( +g ‘ 𝑀 ) 𝑌 ) ∈ 𝐺 ) ) )
50	1 22 26 2	eqgval	⊢ ( ( 𝑀 ∈ Grp ∧ 𝐺 ⊆ 𝐵 ) → ( ( 𝐾 · 𝑋 ) ∼ ( 𝐾 · 𝑌 ) ↔ ( ( 𝐾 · 𝑋 ) ∈ 𝐵 ∧ ( 𝐾 · 𝑌 ) ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝐾 · 𝑌 ) ) ∈ 𝐺 ) ) )
51	43 47 50	syl2anc	⊢ ( 𝜑 → ( ( 𝐾 · 𝑋 ) ∼ ( 𝐾 · 𝑌 ) ↔ ( ( 𝐾 · 𝑋 ) ∈ 𝐵 ∧ ( 𝐾 · 𝑌 ) ∈ 𝐵 ∧ ( ( ( invg ‘ 𝑀 ) ‘ ( 𝐾 · 𝑋 ) ) ( +g ‘ 𝑀 ) ( 𝐾 · 𝑌 ) ) ∈ 𝐺 ) ) )
52	42 49 51	3imtr4d	⊢ ( 𝜑 → ( 𝑋 ∼ 𝑌 → ( 𝐾 · 𝑋 ) ∼ ( 𝐾 · 𝑌 ) ) )