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	biimpi	$⊢ V \in B \to V \in {Base}_{M}$
27	26	adantr	$⊢ (V \in B \land X \in R) \to V \in {Base}_{M}$
28	1	eleq2i	$⊢ W \in B \leftrightarrow W \in {Base}_{M}$
29	28	biimpi	$⊢ W \in B \to W \in {Base}_{M}$
30	29	adantr	$⊢ (W \in B \land Y \in R) \to W \in {Base}_{M}$
31		prelpwi	$⊢ (V \in {Base}_{M} \land W \in {Base}_{M}) \to \{V, W\} \in 𝒫 {Base}_{M}$
32	27 30 31	syl2an	$⊢ ((V \in B \land X \in R) \land (W \in B \land Y \in R)) \to \{V, W\} \in 𝒫 {Base}_{M}$
33	32	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}$
34		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)$
35	8 24 33 34	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)$
36		lmodcmn	$⊢ M \in LMod \to M \in CMnd$
37	36	adantr	$⊢ (M \in LMod \land V \neq W) \to M \in CMnd$
38	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 M \in CMnd$
39		simpr	$⊢ (M \in LMod \land V \neq W) \to V \neq W$
40		simpl	$⊢ (V \in B \land X \in R) \to V \in B$
41		simpl	$⊢ (W \in B \land Y \in R) \to W \in B$
42	39 40 41	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)$
43		3anrot	$⊢ (V \neq W \land V \in B \land W \in B) \leftrightarrow (V \in B \land W \in B \land V \neq W)$
44	42 43	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)$
45	6	a1i	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to F = \{⟨V, X⟩, ⟨W, Y⟩\}$
46	45	fveq1d	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to F (V) = \{⟨V, X⟩, ⟨W, Y⟩\} (V)$
47		simprl	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to V \in B$
48		simprr	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to X \in R$
49	39	adantr	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to V \neq W$
50		fvpr1g	$⊢ (V \in B \land X \in R \land V \neq W) \to \{⟨V, X⟩, ⟨W, Y⟩\} (V) = X$
51	47 48 49 50	syl3anc	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to \{⟨V, X⟩, ⟨W, Y⟩\} (V) = X$
52	46 51	eqtrd	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to F (V) = X$
53	52	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$
54	7	adantr	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to M \in LMod$
55		eqid	$⊢ \cdot_{M} = \cdot_{M}$
56	1 2 55 3	lmodvscl	$⊢ (M \in LMod \land X \in R \land V \in B) \to X \cdot_{M} V \in B$
57	54 48 47 56	syl3anc	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to X \cdot_{M} V \in B$
58	53 57	eqeltrd	$⊢ ((M \in LMod \land V \neq W) \land (V \in B \land X \in R)) \to F (V) \cdot_{M} V \in B$
59	58	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$
60	6	a1i	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to F = \{⟨V, X⟩, ⟨W, Y⟩\}$
61	60	fveq1d	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to F (W) = \{⟨V, X⟩, ⟨W, Y⟩\} (W)$
62		simprl	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to W \in B$
63		simprr	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to Y \in R$
64	39	adantr	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to V \neq W$
65		fvpr2g	$⊢ (W \in B \land Y \in R \land V \neq W) \to \{⟨V, X⟩, ⟨W, Y⟩\} (W) = Y$
66	62 63 64 65	syl3anc	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to \{⟨V, X⟩, ⟨W, Y⟩\} (W) = Y$
67	61 66	eqtrd	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to F (W) = Y$
68	67	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$
69	7	adantr	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to M \in LMod$
70	1 2 55 3	lmodvscl	$⊢ (M \in LMod \land Y \in R \land W \in B) \to Y \cdot_{M} W \in B$
71	69 63 62 70	syl3anc	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to Y \cdot_{M} W \in B$
72	68 71	eqeltrd	$⊢ ((M \in LMod \land V \neq W) \land (W \in B \land Y \in R)) \to F (W) \cdot_{M} W \in B$
73	72	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$
74		fveq2	$⊢ v = V \to F (v) = F (V)$
75		id	$⊢ v = V \to v = V$
76	74 75	oveq12d	$⊢ v = V \to F (v) \cdot_{M} v = F (V) \cdot_{M} V$
77		fveq2	$⊢ v = W \to F (v) = F (W)$
78		id	$⊢ v = W \to v = W$
79	77 78	oveq12d	$⊢ v = W \to F (v) \cdot_{M} v = F (W) \cdot_{M} W$
80	1 5 76 79	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)$
81	38 44 59 73 80	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)$
82	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}$
83	82	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}$
84	6	fveq1i	$⊢ F (V) = \{⟨V, X⟩, ⟨W, Y⟩\} (V)$
85	40	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$
86		simpr	$⊢ (V \in B \land X \in R) \to X \in R$
87	86	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$
88	39	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$
89	85 87 88 50	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$
90	84 89	syl5eq	$⊢ ((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$
91		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$
92	83 90 91	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$
93	6	fveq1i	$⊢ F (W) = \{⟨V, X⟩, ⟨W, Y⟩\} (W)$
94	41	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$
95		simpr	$⊢ (W \in B \land Y \in R) \to Y \in R$
96	95	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$
97	94 96 88 65	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$
98	93 97	syl5eq	$⊢ ((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$
99		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$
100	83 98 99	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$
101	92 100	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)$
102	35 81 101	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