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	$⊢ \underset{˙}{\sim} = M ~_{QG} G$
	eqgvscpbl.s	$⊢ S = {Base}_{Scalar (M)}$
	eqgvscpbl.p	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
	eqgvscpbl.m	$⊢ φ \to M \in LMod$
	eqgvscpbl.g	$⊢ φ \to G \in LSubSp (M)$
	eqgvscpbl.k	$⊢ φ \to K \in S$
Assertion	eqgvscpbl	$⊢ φ \to (X \underset{˙}{\sim} Y \to (K \underset{˙}{\cdot} X) \underset{˙}{\sim} (K \underset{˙}{\cdot} Y))$

Proof

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

Metamath Proof Explorer

Theorem eqgvscpbl

Proof