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	\|- B = ( Base ` M )
	eqgvscpbl.e	\|- .~ = ( M ~QG G )
	eqgvscpbl.s	\|- S = ( Base ` ( Scalar ` M ) )
	eqgvscpbl.p	\|- .x. = ( .s ` M )
	eqgvscpbl.m	\|- ( ph -> M e. LMod )
	eqgvscpbl.g	\|- ( ph -> G e. ( LSubSp ` M ) )
	eqgvscpbl.k	\|- ( ph -> K e. S )
Assertion	eqgvscpbl	\|- ( ph -> ( X .~ Y -> ( K .x. X ) .~ ( K .x. Y ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqgvscpbl.v	\|- B = ( Base ` M )
2		eqgvscpbl.e	\|- .~ = ( M ~QG G )
3		eqgvscpbl.s	\|- S = ( Base ` ( Scalar ` M ) )
4		eqgvscpbl.p	\|- .x. = ( .s ` M )
5		eqgvscpbl.m	\|- ( ph -> M e. LMod )
6		eqgvscpbl.g	\|- ( ph -> G e. ( LSubSp ` M ) )
7		eqgvscpbl.k	\|- ( ph -> K e. S )
8	5	adantr	\|- ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> M e. LMod )
9	7	adantr	\|- ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> K e. S )
10		simpr1	\|- ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> X e. B )
11		eqid	\|- ( Scalar ` M ) = ( Scalar ` M )
12	1 11 4 3	lmodvscl	\|- ( ( M e. LMod /\ K e. S /\ X e. B ) -> ( K .x. X ) e. B )
13	8 9 10 12	syl3anc	\|- ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( K .x. X ) e. B )
14		simpr2	\|- ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> Y e. B )
15	1 11 4 3	lmodvscl	\|- ( ( M e. LMod /\ K e. S /\ Y e. B ) -> ( K .x. Y ) e. B )
16	8 9 14 15	syl3anc	\|- ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( K .x. Y ) e. B )
17	5	ad2antrr	\|- ( ( ( ph /\ X e. B ) /\ Y e. B ) -> M e. LMod )
18	7	ad2antrr	\|- ( ( ( ph /\ X e. B ) /\ Y e. B ) -> K e. S )
19		lmodgrp	\|- ( M e. LMod -> M e. Grp )
20	17 19	syl	\|- ( ( ( ph /\ X e. B ) /\ Y e. B ) -> M e. Grp )
21		simplr	\|- ( ( ( ph /\ X e. B ) /\ Y e. B ) -> X e. B )
22		eqid	\|- ( invg ` M ) = ( invg ` M )
23	1 22	grpinvcl	\|- ( ( M e. Grp /\ X e. B ) -> ( ( invg ` M ) ` X ) e. B )
24	20 21 23	syl2anc	\|- ( ( ( ph /\ X e. B ) /\ Y e. B ) -> ( ( invg ` M ) ` X ) e. B )
25		simpr	\|- ( ( ( ph /\ X e. B ) /\ Y e. B ) -> Y e. B )
26		eqid	\|- ( +g ` M ) = ( +g ` M )
27	1 26 11 4 3	lmodvsdi	\|- ( ( M e. LMod /\ ( K e. S /\ ( ( invg ` M ) ` X ) e. B /\ Y e. B ) ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) = ( ( K .x. ( ( invg ` M ) ` X ) ) ( +g ` M ) ( K .x. Y ) ) )
28	17 18 24 25 27	syl13anc	\|- ( ( ( ph /\ X e. B ) /\ Y e. B ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) = ( ( K .x. ( ( invg ` M ) ` X ) ) ( +g ` M ) ( K .x. Y ) ) )
29	1 11 4 22 3	lmodvsinv2	\|- ( ( M e. LMod /\ K e. S /\ X e. B ) -> ( K .x. ( ( invg ` M ) ` X ) ) = ( ( invg ` M ) ` ( K .x. X ) ) )
30	17 18 21 29	syl3anc	\|- ( ( ( ph /\ X e. B ) /\ Y e. B ) -> ( K .x. ( ( invg ` M ) ` X ) ) = ( ( invg ` M ) ` ( K .x. X ) ) )
31	30	oveq1d	\|- ( ( ( ph /\ X e. B ) /\ Y e. B ) -> ( ( K .x. ( ( invg ` M ) ` X ) ) ( +g ` M ) ( K .x. Y ) ) = ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) )
32	28 31	eqtrd	\|- ( ( ( ph /\ X e. B ) /\ Y e. B ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) = ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) )
33	32	anasss	\|- ( ( ph /\ ( X e. B /\ Y e. B ) ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) = ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) )
34	33	3adantr3	\|- ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) = ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) )
35	6	adantr	\|- ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> G e. ( LSubSp ` M ) )
36		simpr3	\|- ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G )
37		eqid	\|- ( LSubSp ` M ) = ( LSubSp ` M )
38	11 4 3 37	lssvscl	\|- ( ( ( M e. LMod /\ G e. ( LSubSp ` M ) ) /\ ( K e. S /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) e. G )
39	8 35 9 36 38	syl22anc	\|- ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( K .x. ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) ) e. G )
40	34 39	eqeltrrd	\|- ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) e. G )
41	13 16 40	3jca	\|- ( ( ph /\ ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) -> ( ( K .x. X ) e. B /\ ( K .x. Y ) e. B /\ ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) e. G ) )
42	41	ex	\|- ( ph -> ( ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) -> ( ( K .x. X ) e. B /\ ( K .x. Y ) e. B /\ ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) e. G ) ) )
43	5 19	syl	\|- ( ph -> M e. Grp )
44	37	lsssubg	\|- ( ( M e. LMod /\ G e. ( LSubSp ` M ) ) -> G e. ( SubGrp ` M ) )
45	5 6 44	syl2anc	\|- ( ph -> G e. ( SubGrp ` M ) )
46	1	subgss	\|- ( G e. ( SubGrp ` M ) -> G C_ B )
47	45 46	syl	\|- ( ph -> G C_ B )
48	1 22 26 2	eqgval	\|- ( ( M e. Grp /\ G C_ B ) -> ( X .~ Y <-> ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) )
49	43 47 48	syl2anc	\|- ( ph -> ( X .~ Y <-> ( X e. B /\ Y e. B /\ ( ( ( invg ` M ) ` X ) ( +g ` M ) Y ) e. G ) ) )
50	1 22 26 2	eqgval	\|- ( ( M e. Grp /\ G C_ B ) -> ( ( K .x. X ) .~ ( K .x. Y ) <-> ( ( K .x. X ) e. B /\ ( K .x. Y ) e. B /\ ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) e. G ) ) )
51	43 47 50	syl2anc	\|- ( ph -> ( ( K .x. X ) .~ ( K .x. Y ) <-> ( ( K .x. X ) e. B /\ ( K .x. Y ) e. B /\ ( ( ( invg ` M ) ` ( K .x. X ) ) ( +g ` M ) ( K .x. Y ) ) e. G ) ) )
52	42 49 51	3imtr4d	\|- ( ph -> ( X .~ Y -> ( K .x. X ) .~ ( K .x. Y ) ) )

Metamath Proof Explorer

Theorem eqgvscpbl

Proof