lincvalsng

Description: The linear combination over a singleton. (Contributed by AV, 25-May-2019)

	Ref	Expression
Hypotheses	lincvalsn.b	$⊢ B = {Base}_{M}$
	lincvalsn.s	$⊢ S = Scalar (M)$
	lincvalsn.r	$⊢ R = {Base}_{S}$
	lincvalsn.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
Assertion	lincvalsng	$⊢ (M \in LMod \land V \in B \land Y \in R) \to \{⟨V, Y⟩\} linC (M) \{V\} = Y \underset{˙}{\cdot} V$

Proof

Step	Hyp	Ref	Expression
1		lincvalsn.b	$⊢ B = {Base}_{M}$
2		lincvalsn.s	$⊢ S = Scalar (M)$
3		lincvalsn.r	$⊢ R = {Base}_{S}$
4		lincvalsn.t	$⊢ \underset{˙}{\cdot} = \cdot_{M}$
5		simp1	$⊢ (M \in LMod \land V \in B \land Y \in R) \to M \in LMod$
6		simp2	$⊢ (M \in LMod \land V \in B \land Y \in R) \to V \in B$
7	2	fveq2i	$⊢ {Base}_{S} = {Base}_{Scalar (M)}$
8	3 7	eqtri	$⊢ R = {Base}_{Scalar (M)}$
9	8	eleq2i	$⊢ Y \in R \leftrightarrow Y \in {Base}_{Scalar (M)}$
10	9	biimpi	$⊢ Y \in R \to Y \in {Base}_{Scalar (M)}$
11	10	3ad2ant3	$⊢ (M \in LMod \land V \in B \land Y \in R) \to Y \in {Base}_{Scalar (M)}$
12		fvexd	$⊢ (M \in LMod \land V \in B \land Y \in R) \to {Base}_{Scalar (M)} \in V$
13		eqid	$⊢ \{⟨V, Y⟩\} = \{⟨V, Y⟩\}$
14	13	mapsnop	$⊢ (V \in B \land Y \in {Base}_{Scalar (M)} \land {Base}_{Scalar (M)} \in V) \to \{⟨V, Y⟩\} \in ({Base}_{Scalar (M)}^{\{V\}})$
15	6 11 12 14	syl3anc	$⊢ (M \in LMod \land V \in B \land Y \in R) \to \{⟨V, Y⟩\} \in ({Base}_{Scalar (M)}^{\{V\}})$
16		snelpwi	$⊢ V \in {Base}_{M} \to \{V\} \in 𝒫 {Base}_{M}$
17	16 1	eleq2s	$⊢ V \in B \to \{V\} \in 𝒫 {Base}_{M}$
18	17	3ad2ant2	$⊢ (M \in LMod \land V \in B \land Y \in R) \to \{V\} \in 𝒫 {Base}_{M}$
19		lincval	$⊢ (M \in LMod \land \{⟨V, Y⟩\} \in ({Base}_{Scalar (M)}^{\{V\}}) \land \{V\} \in 𝒫 {Base}_{M}) \to \{⟨V, Y⟩\} linC (M) \{V\} = \underset{v \in \{V\}}{\sum_{M}} (\{⟨V, Y⟩\} (v) \cdot_{M} v)$
20	5 15 18 19	syl3anc	$⊢ (M \in LMod \land V \in B \land Y \in R) \to \{⟨V, Y⟩\} linC (M) \{V\} = \underset{v \in \{V\}}{\sum_{M}} (\{⟨V, Y⟩\} (v) \cdot_{M} v)$
21		lmodgrp	$⊢ M \in LMod \to M \in Grp$
22	21	grpmndd	$⊢ M \in LMod \to M \in Mnd$
23	22	3ad2ant1	$⊢ (M \in LMod \land V \in B \land Y \in R) \to M \in Mnd$
24		fvsng	$⊢ (V \in B \land Y \in R) \to \{⟨V, Y⟩\} (V) = Y$
25	24	3adant1	$⊢ (M \in LMod \land V \in B \land Y \in R) \to \{⟨V, Y⟩\} (V) = Y$
26	25	oveq1d	$⊢ (M \in LMod \land V \in B \land Y \in R) \to \{⟨V, Y⟩\} (V) \cdot_{M} V = Y \cdot_{M} V$
27		eqid	$⊢ \cdot_{M} = \cdot_{M}$
28	1 2 27 3	lmodvscl	$⊢ (M \in LMod \land Y \in R \land V \in B) \to Y \cdot_{M} V \in B$
29	28	3com23	$⊢ (M \in LMod \land V \in B \land Y \in R) \to Y \cdot_{M} V \in B$
30	26 29	eqeltrd	$⊢ (M \in LMod \land V \in B \land Y \in R) \to \{⟨V, Y⟩\} (V) \cdot_{M} V \in B$
31		fveq2	$⊢ v = V \to \{⟨V, Y⟩\} (v) = \{⟨V, Y⟩\} (V)$
32		id	$⊢ v = V \to v = V$
33	31 32	oveq12d	$⊢ v = V \to \{⟨V, Y⟩\} (v) \cdot_{M} v = \{⟨V, Y⟩\} (V) \cdot_{M} V$
34	1 33	gsumsn	$⊢ (M \in Mnd \land V \in B \land \{⟨V, Y⟩\} (V) \cdot_{M} V \in B) \to \underset{v \in \{V\}}{\sum_{M}} (\{⟨V, Y⟩\} (v) \cdot_{M} v) = \{⟨V, Y⟩\} (V) \cdot_{M} V$
35	23 6 30 34	syl3anc	$⊢ (M \in LMod \land V \in B \land Y \in R) \to \underset{v \in \{V\}}{\sum_{M}} (\{⟨V, Y⟩\} (v) \cdot_{M} v) = \{⟨V, Y⟩\} (V) \cdot_{M} V$
36	4	eqcomi	$⊢ \cdot_{M} = \underset{˙}{\cdot}$
37	36	a1i	$⊢ (M \in LMod \land V \in B \land Y \in R) \to \cdot_{M} = \underset{˙}{\cdot}$
38		eqidd	$⊢ (M \in LMod \land V \in B \land Y \in R) \to V = V$
39	37 25 38	oveq123d	$⊢ (M \in LMod \land V \in B \land Y \in R) \to \{⟨V, Y⟩\} (V) \cdot_{M} V = Y \underset{˙}{\cdot} V$
40	20 35 39	3eqtrd	$⊢ (M \in LMod \land V \in B \land Y \in R) \to \{⟨V, Y⟩\} linC (M) \{V\} = Y \underset{˙}{\cdot} V$

Metamath Proof Explorer

Theorem lincvalsng

Proof