qusvscpbl

Description: The quotient map distributes over the scalar multiplication. (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$
	qusscaval.n	$⊢ N = M /_{𝑠} (M ~_{QG} G)$
	qusscaval.m	$⊢ \underset{˙}{∙} = \cdot_{N}$
	qusvscpbl.f	$⊢ F = (x \in B ⟼ [x] (M ~_{QG} G))$
	qusvscpbl.u	$⊢ φ \to U \in B$
	qusvscpbl.v	$⊢ φ \to V \in B$
Assertion	qusvscpbl	$⊢ φ \to (F (U) = F (V) \to F (K \underset{˙}{\cdot} U) = F (K \underset{˙}{\cdot} V))$

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		qusscaval.n	$⊢ N = M /_{𝑠} (M ~_{QG} G)$
9		qusscaval.m	$⊢ \underset{˙}{∙} = \cdot_{N}$
10		qusvscpbl.f	$⊢ F = (x \in B ⟼ [x] (M ~_{QG} G))$
11		qusvscpbl.u	$⊢ φ \to U \in B$
12		qusvscpbl.v	$⊢ φ \to V \in B$
13		eqid	$⊢ M ~_{QG} G = M ~_{QG} G$
14	1 13 3 4 5 6 7	eqgvscpbl	$⊢ φ \to (U (M ~_{QG} G) V \to (K \underset{˙}{\cdot} U) (M ~_{QG} G) (K \underset{˙}{\cdot} V))$
15		eqid	$⊢ LSubSp (M) = LSubSp (M)$
16	15	lsssubg	$⊢ (M \in LMod \land G \in LSubSp (M)) \to G \in SubGrp (M)$
17	5 6 16	syl2anc	$⊢ φ \to G \in SubGrp (M)$
18	1 13	eqger	$⊢ G \in SubGrp (M) \to (M ~_{QG} G) Er B$
19	17 18	syl	$⊢ φ \to (M ~_{QG} G) Er B$
20	19 11	erth	$⊢ φ \to (U (M ~_{QG} G) V \leftrightarrow [U] (M ~_{QG} G) = [V] (M ~_{QG} G))$
21		eqid	$⊢ Scalar (M) = Scalar (M)$
22	1 21 4 3	lmodvscl	$⊢ (M \in LMod \land K \in S \land U \in B) \to K \underset{˙}{\cdot} U \in B$
23	5 7 11 22	syl3anc	$⊢ φ \to K \underset{˙}{\cdot} U \in B$
24	19 23	erth	$⊢ φ \to ((K \underset{˙}{\cdot} U) (M ~_{QG} G) (K \underset{˙}{\cdot} V) \leftrightarrow [(K \underset{˙}{\cdot} U)] (M ~_{QG} G) = [(K \underset{˙}{\cdot} V)] (M ~_{QG} G))$
25	14 20 24	3imtr3d	$⊢ φ \to ([U] (M ~_{QG} G) = [V] (M ~_{QG} G) \to [(K \underset{˙}{\cdot} U)] (M ~_{QG} G) = [(K \underset{˙}{\cdot} V)] (M ~_{QG} G))$
26		eceq1	$⊢ x = U \to [x] (M ~_{QG} G) = [U] (M ~_{QG} G)$
27		ovex	$⊢ M ~_{QG} G \in V$
28		ecexg	$⊢ M ~_{QG} G \in V \to [U] (M ~_{QG} G) \in V$
29	27 28	ax-mp	$⊢ [U] (M ~_{QG} G) \in V$
30	26 10 29	fvmpt	$⊢ U \in B \to F (U) = [U] (M ~_{QG} G)$
31	11 30	syl	$⊢ φ \to F (U) = [U] (M ~_{QG} G)$
32		eceq1	$⊢ x = V \to [x] (M ~_{QG} G) = [V] (M ~_{QG} G)$
33		ecexg	$⊢ M ~_{QG} G \in V \to [V] (M ~_{QG} G) \in V$
34	27 33	ax-mp	$⊢ [V] (M ~_{QG} G) \in V$
35	32 10 34	fvmpt	$⊢ V \in B \to F (V) = [V] (M ~_{QG} G)$
36	12 35	syl	$⊢ φ \to F (V) = [V] (M ~_{QG} G)$
37	31 36	eqeq12d	$⊢ φ \to (F (U) = F (V) \leftrightarrow [U] (M ~_{QG} G) = [V] (M ~_{QG} G))$
38		eceq1	$⊢ x = K \underset{˙}{\cdot} U \to [x] (M ~_{QG} G) = [(K \underset{˙}{\cdot} U)] (M ~_{QG} G)$
39		ecexg	$⊢ M ~_{QG} G \in V \to [(K \underset{˙}{\cdot} U)] (M ~_{QG} G) \in V$
40	27 39	ax-mp	$⊢ [(K \underset{˙}{\cdot} U)] (M ~_{QG} G) \in V$
41	38 10 40	fvmpt	$⊢ K \underset{˙}{\cdot} U \in B \to F (K \underset{˙}{\cdot} U) = [(K \underset{˙}{\cdot} U)] (M ~_{QG} G)$
42	23 41	syl	$⊢ φ \to F (K \underset{˙}{\cdot} U) = [(K \underset{˙}{\cdot} U)] (M ~_{QG} G)$
43	1 21 4 3	lmodvscl	$⊢ (M \in LMod \land K \in S \land V \in B) \to K \underset{˙}{\cdot} V \in B$
44	5 7 12 43	syl3anc	$⊢ φ \to K \underset{˙}{\cdot} V \in B$
45		eceq1	$⊢ x = K \underset{˙}{\cdot} V \to [x] (M ~_{QG} G) = [(K \underset{˙}{\cdot} V)] (M ~_{QG} G)$
46		ecexg	$⊢ M ~_{QG} G \in V \to [(K \underset{˙}{\cdot} V)] (M ~_{QG} G) \in V$
47	27 46	ax-mp	$⊢ [(K \underset{˙}{\cdot} V)] (M ~_{QG} G) \in V$
48	45 10 47	fvmpt	$⊢ K \underset{˙}{\cdot} V \in B \to F (K \underset{˙}{\cdot} V) = [(K \underset{˙}{\cdot} V)] (M ~_{QG} G)$
49	44 48	syl	$⊢ φ \to F (K \underset{˙}{\cdot} V) = [(K \underset{˙}{\cdot} V)] (M ~_{QG} G)$
50	42 49	eqeq12d	$⊢ φ \to (F (K \underset{˙}{\cdot} U) = F (K \underset{˙}{\cdot} V) \leftrightarrow [(K \underset{˙}{\cdot} U)] (M ~_{QG} G) = [(K \underset{˙}{\cdot} V)] (M ~_{QG} G))$
51	25 37 50	3imtr4d	$⊢ φ \to (F (U) = F (V) \to F (K \underset{˙}{\cdot} U) = F (K \underset{˙}{\cdot} V))$

Metamath Proof Explorer

Theorem qusvscpbl

Proof