qusscaval

Description: Value of the scalar multiplication operation on the quotient structure. (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}$
Assertion	qusscaval	$⊢ (φ \land K \in S \land X \in B) \to K \underset{˙}{∙} [X] (M ~_{QG} G) = [(K \underset{˙}{\cdot} X)] (M ~_{QG} G)$

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	8	a1i	$⊢ φ \to N = M /_{𝑠} (M ~_{QG} G)$
11	1	a1i	$⊢ φ \to B = {Base}_{M}$
12		eqid	$⊢ (x \in B ⟼ [x] (M ~_{QG} G)) = (x \in B ⟼ [x] (M ~_{QG} G))$
13		ovex	$⊢ M ~_{QG} G \in V$
14	13	a1i	$⊢ φ \to M ~_{QG} G \in V$
15	10 11 12 14 5	qusval	$⊢ φ \to N = (x \in B ⟼ [x] (M ~_{QG} G)) “_{𝑠} M$
16	10 11 12 14 5	quslem	$⊢ φ \to (x \in B ⟼ [x] (M ~_{QG} G)) : B \underset{onto}{⟶} B / (M ~_{QG} G)$
17		eqid	$⊢ Scalar (M) = Scalar (M)$
18	5	adantr	$⊢ (φ \land (k \in S \land u \in B \land v \in B)) \to M \in LMod$
19	6	adantr	$⊢ (φ \land (k \in S \land u \in B \land v \in B)) \to G \in LSubSp (M)$
20		simpr1	$⊢ (φ \land (k \in S \land u \in B \land v \in B)) \to k \in S$
21		simpr2	$⊢ (φ \land (k \in S \land u \in B \land v \in B)) \to u \in B$
22		simpr3	$⊢ (φ \land (k \in S \land u \in B \land v \in B)) \to v \in B$
23	1 2 3 4 18 19 20 8 9 12 21 22	qusvscpbl	$⊢ (φ \land (k \in S \land u \in B \land v \in B)) \to ((x \in B ⟼ [x] (M ~_{QG} G)) (u) = (x \in B ⟼ [x] (M ~_{QG} G)) (v) \to (x \in B ⟼ [x] (M ~_{QG} G)) (k \underset{˙}{\cdot} u) = (x \in B ⟼ [x] (M ~_{QG} G)) (k \underset{˙}{\cdot} v))$
24	15 11 16 5 17 3 4 9 23	imasvscaval	$⊢ (φ \land K \in S \land X \in B) \to K \underset{˙}{∙} (x \in B ⟼ [x] (M ~_{QG} G)) (X) = (x \in B ⟼ [x] (M ~_{QG} G)) (K \underset{˙}{\cdot} X)$
25		eceq1	$⊢ x = X \to [x] (M ~_{QG} G) = [X] (M ~_{QG} G)$
26		ecexg	$⊢ M ~_{QG} G \in V \to [X] (M ~_{QG} G) \in V$
27	13 26	ax-mp	$⊢ [X] (M ~_{QG} G) \in V$
28	25 12 27	fvmpt	$⊢ X \in B \to (x \in B ⟼ [x] (M ~_{QG} G)) (X) = [X] (M ~_{QG} G)$
29	28	3ad2ant3	$⊢ (φ \land K \in S \land X \in B) \to (x \in B ⟼ [x] (M ~_{QG} G)) (X) = [X] (M ~_{QG} G)$
30	29	oveq2d	$⊢ (φ \land K \in S \land X \in B) \to K \underset{˙}{∙} (x \in B ⟼ [x] (M ~_{QG} G)) (X) = K \underset{˙}{∙} [X] (M ~_{QG} G)$
31	1 17 4 3	lmodvscl	$⊢ (M \in LMod \land K \in S \land X \in B) \to K \underset{˙}{\cdot} X \in B$
32	5 31	syl3an1	$⊢ (φ \land K \in S \land X \in B) \to K \underset{˙}{\cdot} X \in B$
33		eceq1	$⊢ x = K \underset{˙}{\cdot} X \to [x] (M ~_{QG} G) = [(K \underset{˙}{\cdot} X)] (M ~_{QG} G)$
34		ecexg	$⊢ M ~_{QG} G \in V \to [(K \underset{˙}{\cdot} X)] (M ~_{QG} G) \in V$
35	13 34	ax-mp	$⊢ [(K \underset{˙}{\cdot} X)] (M ~_{QG} G) \in V$
36	33 12 35	fvmpt	$⊢ K \underset{˙}{\cdot} X \in B \to (x \in B ⟼ [x] (M ~_{QG} G)) (K \underset{˙}{\cdot} X) = [(K \underset{˙}{\cdot} X)] (M ~_{QG} G)$
37	32 36	syl	$⊢ (φ \land K \in S \land X \in B) \to (x \in B ⟼ [x] (M ~_{QG} G)) (K \underset{˙}{\cdot} X) = [(K \underset{˙}{\cdot} X)] (M ~_{QG} G)$
38	24 30 37	3eqtr3d	$⊢ (φ \land K \in S \land X \in B) \to K \underset{˙}{∙} [X] (M ~_{QG} G) = [(K \underset{˙}{\cdot} X)] (M ~_{QG} G)$

Metamath Proof Explorer

Theorem qusscaval

Proof