lincvalpr

Description: The linear combination over an unordered pair. (Contributed by AV, 16-Apr-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}$
	lincvalpr.p	$⊢ \underset{˙}{+} = +_{M}$
	lincvalpr.f	$⊢ F = \{⟨V, X⟩, ⟨W, Y⟩\}$
Assertion	lincvalpr	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to F linC (M) \{V, W\} = (X \underset{˙}{\cdot} V) \underset{˙}{+} (Y \underset{˙}{\cdot} W)$

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		lincvalpr.p	$⊢ \underset{˙}{+} = +_{M}$
6		lincvalpr.f	$⊢ F = \{⟨V, X⟩, ⟨W, Y⟩\}$
7		simpl	$⊢ (M \in LMod \land V \neq W) \to M \in LMod$
8	7	3ad2ant1	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to M \in LMod$
9	2	fveq2i	$⊢ {Base}_{S} = {Base}_{Scalar (M)}$
10	3 9	eqtri	$⊢ R = {Base}_{Scalar (M)}$
11	10	eleq2i	$⊢ X \in R \leftrightarrow X \in {Base}_{Scalar (M)}$
12	11	biimpi	$⊢ X \in R \to X \in {Base}_{Scalar (M)}$
13	12	anim2i	$⊢ (V \in B \land X \in R) \to (V \in B \land X \in {Base}_{Scalar (M)})$
14	13	3ad2ant2	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to (V \in B \land X \in {Base}_{Scalar (M)})$
15	10	eleq2i	$⊢ Y \in R \leftrightarrow Y \in {Base}_{Scalar (M)}$
16	15	biimpi	$⊢ Y \in R \to Y \in {Base}_{Scalar (M)}$
17	16	anim2i	$⊢ (W \in B \land Y \in R) \to (W \in B \land Y \in {Base}_{Scalar (M)})$
18	17	3ad2ant3	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to (W \in B \land Y \in {Base}_{Scalar (M)})$
19		fvexd	$⊢ M \in LMod \to {Base}_{Scalar (M)} \in V$
20	19	anim2i	$⊢ (V \neq W \land M \in LMod) \to (V \neq W \land {Base}_{Scalar (M)} \in V)$
21	20	ancoms	$⊢ (M \in LMod \land V \neq W) \to (V \neq W \land {Base}_{Scalar (M)} \in V)$
22	21	3ad2ant1	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to (V \neq W \land {Base}_{Scalar (M)} \in V)$
23	6	mapprop	$⊢ ((V \in B \land X \in {Base}_{Scalar (M)}) \land (W \in B \land Y \in {Base}_{Scalar (M)}) \land (V \neq W \land {Base}_{Scalar (M)} \in V)) \to F \in ({Base}_{Scalar (M)}^{\{V, W\}})$
24	14 18 22 23	syl3anc	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to F \in ({Base}_{Scalar (M)}^{\{V, W\}})$
25	1	eleq2i	$⊢ V \in B \leftrightarrow V \in {Base}_{M}$
26	25	birani	$⊢ (V \in B \land X \in R) \to V \in {Base}_{M}$
27	1	eleq2i	$⊢ W \in B \leftrightarrow W \in {Base}_{M}$
28	27	birani	$⊢ (W \in B \land Y \in R) \to W \in {Base}_{M}$
29		prelpwi	$⊢ (V \in {Base}_{M} \land W \in {Base}_{M}) \to \{V, W\} \in 𝒫 {Base}_{M}$
30	26 28 29	syl2an	$⊢ ((V \in B \land X \in R) \land (W \in B \land Y \in R)) \to \{V, W\} \in 𝒫 {Base}_{M}$
31	30	3adant1	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to \{V, W\} \in 𝒫 {Base}_{M}$
32		lincval	$⊢ (M \in LMod \land F \in ({Base}_{Scalar (M)}^{\{V, W\}}) \land \{V, W\} \in 𝒫 {Base}_{M}) \to F linC (M) \{V, W\} = \underset{v \in \{V, W\}}{\sum_{M}} (F (v) \cdot_{M} v)$
33	8 24 31 32	syl3anc	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to F linC (M) \{V, W\} = \underset{v \in \{V, W\}}{\sum_{M}} (F (v) \cdot_{M} v)$
34		lmodcmn	$⊢ M \in LMod \to M \in CMnd$
35	34	adantr	$⊢ (M \in LMod \land V \neq W) \to M \in CMnd$
36	35	3ad2ant1	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to M \in CMnd$
37		simpr	$⊢ (M \in LMod \land V \neq W) \to V \neq W$
38		simpl	$⊢ (V \in B \land X \in R) \to V \in B$
39		simpl	$⊢ (W \in B \land Y \in R) \to W \in B$
40	37 38 39	3anim123i	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to (V \neq W \land V \in B \land W \in B)$
41		3anrot	$⊢ (V \neq W \land V \in B \land W \in B) \leftrightarrow (V \in B \land W \in B \land V \neq W)$
42	40 41	sylib	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to (V \in B \land W \in B \land V \neq W)$
43	6	a1i	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to F = \{⟨V, X⟩, ⟨W, Y⟩\}$
44	43	fveq1d	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to F (V) = \{⟨V, X⟩, ⟨W, Y⟩\} (V)$
45		simprl	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to V \in B$
46		simprr	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to X \in R$
47	37	adantr	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to V \neq W$
48		fvpr1g	$⊢ (V \in B \land X \in R \land V \neq W) \to \{⟨V, X⟩, ⟨W, Y⟩\} (V) = X$
49	45 46 47 48	syl3anc	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to \{⟨V, X⟩, ⟨W, Y⟩\} (V) = X$
50	44 49	eqtrd	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to F (V) = X$
51	50	oveq1d	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to F (V) \cdot_{M} V = X \cdot_{M} V$
52	7	adantr	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to M \in LMod$
53		eqid	$⊢ \cdot_{M} = \cdot_{M}$
54	1 2 53 3	lmodvscl	$⊢ (M \in LMod \land X \in R \land V \in B) \to X \cdot_{M} V \in B$
55	52 46 45 54	syl3anc	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to X \cdot_{M} V \in B$
56	51 55	eqeltrd	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to F (V) \cdot_{M} V \in B$
57	56	3adant3	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to F (V) \cdot_{M} V \in B$
58	6	a1i	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to F = \{⟨V, X⟩, ⟨W, Y⟩\}$
59	58	fveq1d	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to F (W) = \{⟨V, X⟩, ⟨W, Y⟩\} (W)$
60		simprl	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to W \in B$
61		simprr	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to Y \in R$
62	37	adantr	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to V \neq W$
63		fvpr2g	$⊢ (W \in B \land Y \in R \land V \neq W) \to \{⟨V, X⟩, ⟨W, Y⟩\} (W) = Y$
64	60 61 62 63	syl3anc	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to \{⟨V, X⟩, ⟨W, Y⟩\} (W) = Y$
65	59 64	eqtrd	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to F (W) = Y$
66	65	oveq1d	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to F (W) \cdot_{M} W = Y \cdot_{M} W$
67	7	adantr	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to M \in LMod$
68	1 2 53 3	lmodvscl	$⊢ (M \in LMod \land Y \in R \land W \in B) \to Y \cdot_{M} W \in B$
69	67 61 60 68	syl3anc	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to Y \cdot_{M} W \in B$
70	66 69	eqeltrd	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to F (W) \cdot_{M} W \in B$
71	70	3adant2	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to F (W) \cdot_{M} W \in B$
72		fveq2	$⊢ v = V \to F (v) = F (V)$
73		id	$⊢ v = V \to v = V$
74	72 73	oveq12d	$⊢ v = V \to F (v) \cdot_{M} v = F (V) \cdot_{M} V$
75		fveq2	$⊢ v = W \to F (v) = F (W)$
76		id	$⊢ v = W \to v = W$
77	75 76	oveq12d	$⊢ v = W \to F (v) \cdot_{M} v = F (W) \cdot_{M} W$
78	1 5 74 77	gsumpr	$⊢ (M \in CMnd \land (V \in B \land W \in B \land V \neq W) \land (F (V) \cdot_{M} V \in B \land F (W) \cdot_{M} W \in B)) \to \underset{v \in \{V, W\}}{\sum_{M}} (F (v) \cdot_{M} v) = (F (V) \cdot_{M} V) \underset{˙}{+} (F (W) \cdot_{M} W)$
79	36 42 57 71 78	syl112anc	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to \underset{v \in \{V, W\}}{\sum_{M}} (F (v) \cdot_{M} v) = (F (V) \cdot_{M} V) \underset{˙}{+} (F (W) \cdot_{M} W)$
80	4	a1i	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to \underset{˙}{\cdot} = \cdot_{M}$
81	80	eqcomd	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to \cdot_{M} = \underset{˙}{\cdot}$
82	6	fveq1i	$⊢ F (V) = \{⟨V, X⟩, ⟨W, Y⟩\} (V)$
83	38	3ad2ant2	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to V \in B$
84		simpr	$⊢ (V \in B \land X \in R) \to X \in R$
85	84	3ad2ant2	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to X \in R$
86	37	3ad2ant1	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to V \neq W$
87	83 85 86 48	syl3anc	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to \{⟨V, X⟩, ⟨W, Y⟩\} (V) = X$
88	82 87	eqtrid	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to F (V) = X$
89		eqidd	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to V = V$
90	81 88 89	oveq123d	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to F (V) \cdot_{M} V = X \underset{˙}{\cdot} V$
91	6	fveq1i	$⊢ F (W) = \{⟨V, X⟩, ⟨W, Y⟩\} (W)$
92	39	3ad2ant3	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to W \in B$
93		simpr	$⊢ (W \in B \land Y \in R) \to Y \in R$
94	93	3ad2ant3	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to Y \in R$
95	92 94 86 63	syl3anc	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to \{⟨V, X⟩, ⟨W, Y⟩\} (W) = Y$
96	91 95	eqtrid	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to F (W) = Y$
97		eqidd	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to W = W$
98	81 96 97	oveq123d	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to F (W) \cdot_{M} W = Y \underset{˙}{\cdot} W$
99	90 98	oveq12d	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to (F (V) \cdot_{M} V) \underset{˙}{+} (F (W) \cdot_{M} W) = (X \underset{˙}{\cdot} V) \underset{˙}{+} (Y \underset{˙}{\cdot} W)$
100	33 79 99	3eqtrd	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R) \land (W \in B \land Y \in R)) \to F linC (M) \{V, W\} = (X \underset{˙}{\cdot} V) \underset{˙}{+} (Y \underset{˙}{\cdot} W)$

Metamath Proof Explorer

Theorem lincvalpr

Proof