Theorem lincvalpr 49118

Description: The linear combination over an unordered pair. (Contributed by AV, 16-Apr-2019.)

Hypotheses

Ref	Expression
lincvalsn.b	⊢ 𝐵 = (Base‘𝑀)
lincvalsn.s	⊢ 𝑆 = (Scalar‘𝑀)
lincvalsn.r	⊢ 𝑅 = (Base‘𝑆)
lincvalsn.t	⊢ · = ( ·𝑠 ‘𝑀)
lincvalpr.p	⊢ + = (+g‘𝑀)
lincvalpr.f	⊢ 𝐹 = {⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}

Assertion

Ref	Expression
lincvalpr	⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = ((𝑋 · 𝑉) + (𝑌 · 𝑊)))

Proof of Theorem lincvalpr

Dummy variable 𝑣 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpl 487	. . . 4 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → 𝑀 ∈ LMod)
2	1	3ad2ant1 1149	. . 3 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑀 ∈ LMod)
3		lincvalsn.r	. . . . . . . . 9 ⊢ 𝑅 = (Base‘𝑆)
4		lincvalsn.s	. . . . . . . . . 10 ⊢ 𝑆 = (Scalar‘𝑀)
5	4	fveq2i 6885	. . . . . . . . 9 ⊢ (Base‘𝑆) = (Base‘(Scalar‘𝑀))
6	3, 5	eqtri 2792	. . . . . . . 8 ⊢ 𝑅 = (Base‘(Scalar‘𝑀))
7	6	eleq2i 2861	. . . . . . 7 ⊢ (𝑋 ∈ 𝑅 ↔ 𝑋 ∈ (Base‘(Scalar‘𝑀)))
8	7	biimpi 219	. . . . . 6 ⊢ (𝑋 ∈ 𝑅 → 𝑋 ∈ (Base‘(Scalar‘𝑀)))
9	8	anim2i 628	. . . . 5 ⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ (Base‘(Scalar‘𝑀))))
10	9	3ad2ant2 1150	. . . 4 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ (Base‘(Scalar‘𝑀))))
11	6	eleq2i 2861	. . . . . . 7 ⊢ (𝑌 ∈ 𝑅 ↔ 𝑌 ∈ (Base‘(Scalar‘𝑀)))
12	11	biimpi 219	. . . . . 6 ⊢ (𝑌 ∈ 𝑅 → 𝑌 ∈ (Base‘(Scalar‘𝑀)))
13	12	anim2i 628	. . . . 5 ⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ (Base‘(Scalar‘𝑀))))
14	13	3ad2ant3 1151	. . . 4 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ (Base‘(Scalar‘𝑀))))
15		fvexd 6897	. . . . . . 7 ⊢ (𝑀 ∈ LMod → (Base‘(Scalar‘𝑀)) ∈ V)
16	15	anim2i 628	. . . . . 6 ⊢ ((𝑉 ≠ 𝑊 ∧ 𝑀 ∈ LMod) → (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V))
17	16	ancoms 463	. . . . 5 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V))
18	17	3ad2ant1 1149	. . . 4 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V))
19		lincvalpr.f	. . . . 5 ⊢ 𝐹 = {⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}
20	19	mapprop 49046	. . . 4 ⊢ (((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ (Base‘(Scalar‘𝑀))) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ (Base‘(Scalar‘𝑀))) ∧ (𝑉 ≠ 𝑊 ∧ (Base‘(Scalar‘𝑀)) ∈ V)) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m {𝑉, 𝑊}))
21	10, 14, 18, 20	syl3anc 1396	. . 3 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m {𝑉, 𝑊}))
22		lincvalsn.b	. . . . . . 7 ⊢ 𝐵 = (Base‘𝑀)
23	22	eleq2i 2861	. . . . . 6 ⊢ (𝑉 ∈ 𝐵 ↔ 𝑉 ∈ (Base‘𝑀))
24	23	birani 508	. . . . 5 ⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → 𝑉 ∈ (Base‘𝑀))
25	22	eleq2i 2861	. . . . . 6 ⊢ (𝑊 ∈ 𝐵 ↔ 𝑊 ∈ (Base‘𝑀))
26	25	birani 508	. . . . 5 ⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → 𝑊 ∈ (Base‘𝑀))
27		prelpwi 5429	. . . . 5 ⊢ ((𝑉 ∈ (Base‘𝑀) ∧ 𝑊 ∈ (Base‘𝑀)) → {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀))
28	24, 26, 27	syl2an 607	. . . 4 ⊢ (((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀))
29	28	3adant1 1146	. . 3 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀))
30		lincval 49109	. . 3 ⊢ ((𝑀 ∈ LMod ∧ 𝐹 ∈ ((Base‘(Scalar‘𝑀)) ↑m {𝑉, 𝑊}) ∧ {𝑉, 𝑊} ∈ 𝒫 (Base‘𝑀)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠 ‘𝑀)𝑣))))
31	2, 21, 29, 30	syl3anc 1396	. 2 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠 ‘𝑀)𝑣))))
32		lmodcmn 21009	. . . . 5 ⊢ (𝑀 ∈ LMod → 𝑀 ∈ CMnd)
33	32	adantr 485	. . . 4 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → 𝑀 ∈ CMnd)
34	33	3ad2ant1 1149	. . 3 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑀 ∈ CMnd)
35		simpr 489	. . . . 5 ⊢ ((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) → 𝑉 ≠ 𝑊)
36		simpl 487	. . . . 5 ⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → 𝑉 ∈ 𝐵)
37		simpl 487	. . . . 5 ⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → 𝑊 ∈ 𝐵)
38	35, 36, 37	3anim123i 1167	. . . 4 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ≠ 𝑊 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵))
39		3anrot 1115	. . . 4 ⊢ ((𝑉 ≠ 𝑊 ∧ 𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵) ↔ (𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊))
40	38, 39	sylib 221	. . 3 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊))
41	19	a1i 11	. . . . . . . 8 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝐹 = {⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩})
42	41	fveq1d 6884	. . . . . . 7 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → (𝐹‘𝑉) = ({⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}‘𝑉))
43		simprl 782	. . . . . . . 8 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑉 ∈ 𝐵)
44		simprr 784	. . . . . . . 8 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑋 ∈ 𝑅)
45	35	adantr 485	. . . . . . . 8 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑉 ≠ 𝑊)
46		fvpr1g 7189	. . . . . . . 8 ⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅 ∧ 𝑉 ≠ 𝑊) → ({⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}‘𝑉) = 𝑋)
47	43, 44, 45, 46	syl3anc 1396	. . . . . . 7 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → ({⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}‘𝑉) = 𝑋)
48	42, 47	eqtrd 2804	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → (𝐹‘𝑉) = 𝑋)
49	48	oveq1d 7426	. . . . 5 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠 ‘𝑀)𝑉) = (𝑋( ·𝑠 ‘𝑀)𝑉))
50	1	adantr 485	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → 𝑀 ∈ LMod)
51		eqid 2769	. . . . . . 7 ⊢ ( ·𝑠 ‘𝑀) = ( ·𝑠 ‘𝑀)
52	22, 4, 51, 3	lmodvscl 20977	. . . . . 6 ⊢ ((𝑀 ∈ LMod ∧ 𝑋 ∈ 𝑅 ∧ 𝑉 ∈ 𝐵) → (𝑋( ·𝑠 ‘𝑀)𝑉) ∈ 𝐵)
53	50, 44, 43, 52	syl3anc 1396	. . . . 5 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → (𝑋( ·𝑠 ‘𝑀)𝑉) ∈ 𝐵)
54	49, 53	eqeltrd 2869	. . . 4 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠 ‘𝑀)𝑉) ∈ 𝐵)
55	54	3adant3 1148	. . 3 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠 ‘𝑀)𝑉) ∈ 𝐵)
56	19	a1i 11	. . . . . . . 8 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝐹 = {⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩})
57	56	fveq1d 6884	. . . . . . 7 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑊) = ({⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}‘𝑊))
58		simprl 782	. . . . . . . 8 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑊 ∈ 𝐵)
59		simprr 784	. . . . . . . 8 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ 𝑅)
60	35	adantr 485	. . . . . . . 8 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 ≠ 𝑊)
61		fvpr2g 7190	. . . . . . . 8 ⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅 ∧ 𝑉 ≠ 𝑊) → ({⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}‘𝑊) = 𝑌)
62	58, 59, 60, 61	syl3anc 1396	. . . . . . 7 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ({⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}‘𝑊) = 𝑌)
63	57, 62	eqtrd 2804	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑊) = 𝑌)
64	63	oveq1d 7426	. . . . 5 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠 ‘𝑀)𝑊) = (𝑌( ·𝑠 ‘𝑀)𝑊))
65	1	adantr 485	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑀 ∈ LMod)
66	22, 4, 51, 3	lmodvscl 20977	. . . . . 6 ⊢ ((𝑀 ∈ LMod ∧ 𝑌 ∈ 𝑅 ∧ 𝑊 ∈ 𝐵) → (𝑌( ·𝑠 ‘𝑀)𝑊) ∈ 𝐵)
67	65, 59, 58, 66	syl3anc 1396	. . . . 5 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑌( ·𝑠 ‘𝑀)𝑊) ∈ 𝐵)
68	64, 67	eqeltrd 2869	. . . 4 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠 ‘𝑀)𝑊) ∈ 𝐵)
69	68	3adant2 1147	. . 3 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠 ‘𝑀)𝑊) ∈ 𝐵)
70		lincvalpr.p	. . . 4 ⊢ + = (+g‘𝑀)
71		fveq2 6882	. . . . 5 ⊢ (𝑣 = 𝑉 → (𝐹‘𝑣) = (𝐹‘𝑉))
72		id 23	. . . . 5 ⊢ (𝑣 = 𝑉 → 𝑣 = 𝑉)
73	71, 72	oveq12d 7429	. . . 4 ⊢ (𝑣 = 𝑉 → ((𝐹‘𝑣)( ·𝑠 ‘𝑀)𝑣) = ((𝐹‘𝑉)( ·𝑠 ‘𝑀)𝑉))
74		fveq2 6882	. . . . 5 ⊢ (𝑣 = 𝑊 → (𝐹‘𝑣) = (𝐹‘𝑊))
75		id 23	. . . . 5 ⊢ (𝑣 = 𝑊 → 𝑣 = 𝑊)
76	74, 75	oveq12d 7429	. . . 4 ⊢ (𝑣 = 𝑊 → ((𝐹‘𝑣)( ·𝑠 ‘𝑀)𝑣) = ((𝐹‘𝑊)( ·𝑠 ‘𝑀)𝑊))
77	22, 70, 73, 76	gsumpr 20025	. . 3 ⊢ ((𝑀 ∈ CMnd ∧ (𝑉 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ≠ 𝑊) ∧ (((𝐹‘𝑉)( ·𝑠 ‘𝑀)𝑉) ∈ 𝐵 ∧ ((𝐹‘𝑊)( ·𝑠 ‘𝑀)𝑊) ∈ 𝐵)) → (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠 ‘𝑀)𝑣))) = (((𝐹‘𝑉)( ·𝑠 ‘𝑀)𝑉) + ((𝐹‘𝑊)( ·𝑠 ‘𝑀)𝑊)))
78	34, 40, 55, 69, 77	syl112anc 1399	. 2 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝑀 Σg (𝑣 ∈ {𝑉, 𝑊} ↦ ((𝐹‘𝑣)( ·𝑠 ‘𝑀)𝑣))) = (((𝐹‘𝑉)( ·𝑠 ‘𝑀)𝑉) + ((𝐹‘𝑊)( ·𝑠 ‘𝑀)𝑊)))
79		lincvalsn.t	. . . . . 6 ⊢ · = ( ·𝑠 ‘𝑀)
80	79	a1i 11	. . . . 5 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → · = ( ·𝑠 ‘𝑀))
81	80	eqcomd 2775	. . . 4 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ( ·𝑠 ‘𝑀) = · )
82	19	fveq1i 6883	. . . . 5 ⊢ (𝐹‘𝑉) = ({⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}‘𝑉)
83	36	3ad2ant2 1150	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 ∈ 𝐵)
84		simpr 489	. . . . . . 7 ⊢ ((𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) → 𝑋 ∈ 𝑅)
85	84	3ad2ant2 1150	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑋 ∈ 𝑅)
86	35	3ad2ant1 1149	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 ≠ 𝑊)
87	83, 85, 86, 46	syl3anc 1396	. . . . 5 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ({⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}‘𝑉) = 𝑋)
88	82, 87	eqtrid 2816	. . . 4 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑉) = 𝑋)
89		eqidd 2770	. . . 4 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑉 = 𝑉)
90	81, 88, 89	oveq123d 7432	. . 3 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑉)( ·𝑠 ‘𝑀)𝑉) = (𝑋 · 𝑉))
91	19	fveq1i 6883	. . . . 5 ⊢ (𝐹‘𝑊) = ({⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}‘𝑊)
92	37	3ad2ant3 1151	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑊 ∈ 𝐵)
93		simpr 489	. . . . . . 7 ⊢ ((𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅) → 𝑌 ∈ 𝑅)
94	93	3ad2ant3 1151	. . . . . 6 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑌 ∈ 𝑅)
95	92, 94, 86, 61	syl3anc 1396	. . . . 5 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ({⟨𝑉, 𝑋⟩, ⟨𝑊, 𝑌⟩}‘𝑊) = 𝑌)
96	91, 95	eqtrid 2816	. . . 4 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹‘𝑊) = 𝑌)
97		eqidd 2770	. . . 4 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → 𝑊 = 𝑊)
98	81, 96, 97	oveq123d 7432	. . 3 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → ((𝐹‘𝑊)( ·𝑠 ‘𝑀)𝑊) = (𝑌 · 𝑊))
99	90, 98	oveq12d 7429	. 2 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (((𝐹‘𝑉)( ·𝑠 ‘𝑀)𝑉) + ((𝐹‘𝑊)( ·𝑠 ‘𝑀)𝑊)) = ((𝑋 · 𝑉) + (𝑌 · 𝑊)))
100	31, 78, 99	3eqtrd 2808	1 ⊢ (((𝑀 ∈ LMod ∧ 𝑉 ≠ 𝑊) ∧ (𝑉 ∈ 𝐵 ∧ 𝑋 ∈ 𝑅) ∧ (𝑊 ∈ 𝐵 ∧ 𝑌 ∈ 𝑅)) → (𝐹( linC ‘𝑀){𝑉, 𝑊}) = ((𝑋 · 𝑉) + (𝑌 · 𝑊)))

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101   = wceq 1567   ∈ wcel 2149   ≠ wne 2964  Vcvv 3461  𝒫 cpw 4565  {cpr 4594  ⟨cop 4598   ↦ cmpt 5194  ‘cfv 6537  (class class class)co 7411   ↑_m cmap 8824  Basecbs 17269  +_gcplusg 17310  Scalarcsca 17313   ·_𝑠 cvsca 17314   Σ_g cgsu 17493  CMndccmn 19850  LModclmod 20959   linC clinc 49104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-10 2182  ax-11 2198  ax-12 2219  ax-ext 2741  ax-rep 5240  ax-sep 5259  ax-nul 5271  ax-pow 5337  ax-pr 5405  ax-un 7733  ax-cnex 11156  ax-resscn 11157  ax-1cn 11158  ax-icn 11159  ax-addcl 11160  ax-addrcl 11161  ax-mulcl 11162  ax-mulrcl 11163  ax-mulcom 11164  ax-addass 11165  ax-mulass 11166  ax-distr 11167  ax-i2m1 11168  ax-1ne0 11169  ax-1rid 11170  ax-rnegex 11171  ax-rrecex 11172  ax-cnre 11173  ax-pre-lttri 11174  ax-pre-lttrn 11175  ax-pre-ltadd 11176  ax-pre-mulgt0 11177

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3or 1102  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-nf 1811  df-sb 2098  df-mo 2573  df-eu 2603  df-clab 2748  df-cleq 2761  df-clel 2844  df-nfc 2918  df-ne 2965  df-nel 3071  df-ral 3086  df-rex 3096  df-rmo 3375  df-reu 3376  df-rab 3423  df-v 3463  df-sbc 3752  df-csb 3860  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-pss 3931  df-nul 4293  df-if 4491  df-pw 4567  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-int 4915  df-iun 4960  df-iin 4961  df-br 5112  df-opab 5176  df-mpt 5195  df-tr 5221  df-id 5557  df-eprel 5562  df-po 5570  df-so 5571  df-fr 5615  df-se 5616  df-we 5617  df-xp 5668  df-rel 5669  df-cnv 5670  df-co 5671  df-dm 5672  df-rn 5673  df-res 5674  df-ima 5675  df-pred 6303  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6493  df-fun 6539  df-fn 6540  df-f 6541  df-f1 6542  df-fo 6543  df-f1o 6544  df-fv 6545  df-isom 6546  df-riota 7368  df-ov 7414  df-oprab 7415  df-mpo 7416  df-of 7675  df-om 7863  df-1st 7986  df-2nd 7987  df-supp 8157  df-frecs 8278  df-wrecs 8309  df-recs 8358  df-rdg 8397  df-1o 8453  df-2o 8454  df-er 8694  df-map 8826  df-en 8944  df-dom 8945  df-sdom 8946  df-fin 8947  df-fsupp 9322  df-oi 9472  df-card 9925  df-pnf 11245  df-mnf 11246  df-xr 11247  df-ltxr 11248  df-le 11249  df-sub 11443  df-neg 11444  df-nn 12234  df-2 12303  df-n0 12505  df-z 12592  df-uz 12863  df-fz 13536  df-fzo 13683  df-seq 14038  df-hash 14367  df-sets 17224  df-slot 17242  df-ndx 17254  df-base 17270  df-ress 17291  df-plusg 17323  df-0g 17494  df-gsum 17495  df-mre 17638  df-mrc 17639  df-acs 17641  df-mgm 18698  df-sgrp 18777  df-mnd 18793  df-submnd 18842  df-grp 19003  df-minusg 19004  df-mulg 19134  df-cntz 19387  df-cmn 19852  df-abl 19853  df-mgp 20217  df-ur 20264  df-ring 20317  df-lmod 20961  df-linc 49106

This theorem is referenced by:  ldepspr  49173