qusvsval

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

Metamath Proof Explorer

Theorem qusvsval

Proof