Metamath Proof Explorer

Theorem lincvalpr

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

Ref Expression
Hypotheses lincvalsn.b ⊢B=BaseM
lincvalsn.s ⊢S=Scalar⁡M
lincvalsn.r ⊢R=BaseS
lincvalsn.t ⊢·˙=⋅M
lincvalpr.p ⊢+˙=+M
lincvalpr.f ⊢F=VXWY
Assertion lincvalpr ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→FlinC⁡MVW=X·˙V+˙Y·˙W

Proof

Step Hyp Ref Expression
1 lincvalsn.b ⊢B=BaseM
2 lincvalsn.s ⊢S=Scalar⁡M
3 lincvalsn.r ⊢R=BaseS
4 lincvalsn.t ⊢·˙=⋅M
5 lincvalpr.p ⊢+˙=+M
6 lincvalpr.f ⊢F=VXWY
7 simpl ⊢M∈LMod∧V≠W→M∈LMod
8 7 3ad2ant1 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→M∈LMod
9 2 fveq2i ⊢BaseS=BaseScalar⁡M
10 3 9 eqtri ⊢R=BaseScalar⁡M
11 10 eleq2i ⊢X∈R↔X∈BaseScalar⁡M
12 11 biimpi ⊢X∈R→X∈BaseScalar⁡M
13 12 anim2i ⊢V∈B∧X∈R→V∈B∧X∈BaseScalar⁡M
14 13 3ad2ant2 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→V∈B∧X∈BaseScalar⁡M
15 10 eleq2i ⊢Y∈R↔Y∈BaseScalar⁡M
16 15 biimpi ⊢Y∈R→Y∈BaseScalar⁡M
17 16 anim2i ⊢W∈B∧Y∈R→W∈B∧Y∈BaseScalar⁡M
18 17 3ad2ant3 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→W∈B∧Y∈BaseScalar⁡M
19 fvexd ⊢M∈LMod→BaseScalar⁡M∈V
20 19 anim2i ⊢V≠W∧M∈LMod→V≠W∧BaseScalar⁡M∈V
21 20 ancoms ⊢M∈LMod∧V≠W→V≠W∧BaseScalar⁡M∈V
22 21 3ad2ant1 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→V≠W∧BaseScalar⁡M∈V
23 6 mapprop ⊢V∈B∧X∈BaseScalar⁡M∧W∈B∧Y∈BaseScalar⁡M∧V≠W∧BaseScalar⁡M∈V→F∈BaseScalar⁡MVW
24 14 18 22 23 syl3anc ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→F∈BaseScalar⁡MVW
25 1 eleq2i ⊢V∈B↔V∈BaseM
26 25 biimpi ⊢V∈B→V∈BaseM
27 26 adantr ⊢V∈B∧X∈R→V∈BaseM
28 1 eleq2i ⊢W∈B↔W∈BaseM
29 28 biimpi ⊢W∈B→W∈BaseM
30 29 adantr ⊢W∈B∧Y∈R→W∈BaseM
31 prelpwi ⊢V∈BaseM∧W∈BaseM→VW∈𝒫BaseM
32 27 30 31 syl2an ⊢V∈B∧X∈R∧W∈B∧Y∈R→VW∈𝒫BaseM
33 32 3adant1 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→VW∈𝒫BaseM
34 lincval ⊢M∈LMod∧F∈BaseScalar⁡MVW∧VW∈𝒫BaseM→FlinC⁡MVW=∑Mv∈VWF⁡v⋅Mv
35 8 24 33 34 syl3anc ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→FlinC⁡MVW=∑Mv∈VWF⁡v⋅Mv
36 lmodcmn ⊢M∈LMod→M∈CMnd
37 36 adantr ⊢M∈LMod∧V≠W→M∈CMnd
38 37 3ad2ant1 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→M∈CMnd
39 simpr ⊢M∈LMod∧V≠W→V≠W
40 simpl ⊢V∈B∧X∈R→V∈B
41 simpl ⊢W∈B∧Y∈R→W∈B
42 39 40 41 3anim123i ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→V≠W∧V∈B∧W∈B
43 3anrot ⊢V≠W∧V∈B∧W∈B↔V∈B∧W∈B∧V≠W
44 42 43 sylib ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→V∈B∧W∈B∧V≠W
45 6 a1i ⊢M∈LMod∧V≠W∧V∈B∧X∈R→F=VXWY
46 45 fveq1d ⊢M∈LMod∧V≠W∧V∈B∧X∈R→F⁡V=VXWY⁡V
47 simprl ⊢M∈LMod∧V≠W∧V∈B∧X∈R→V∈B
48 simprr ⊢M∈LMod∧V≠W∧V∈B∧X∈R→X∈R
49 39 adantr ⊢M∈LMod∧V≠W∧V∈B∧X∈R→V≠W
50 fvpr1g ⊢V∈B∧X∈R∧V≠W→VXWY⁡V=X
51 47 48 49 50 syl3anc ⊢M∈LMod∧V≠W∧V∈B∧X∈R→VXWY⁡V=X
52 46 51 eqtrd ⊢M∈LMod∧V≠W∧V∈B∧X∈R→F⁡V=X
53 52 oveq1d ⊢M∈LMod∧V≠W∧V∈B∧X∈R→F⁡V⋅MV=X⋅MV
54 7 adantr ⊢M∈LMod∧V≠W∧V∈B∧X∈R→M∈LMod
55 eqid ⊢⋅M=⋅M
56 1 2 55 3 lmodvscl ⊢M∈LMod∧X∈R∧V∈B→X⋅MV∈B
57 54 48 47 56 syl3anc ⊢M∈LMod∧V≠W∧V∈B∧X∈R→X⋅MV∈B
58 53 57 eqeltrd ⊢M∈LMod∧V≠W∧V∈B∧X∈R→F⁡V⋅MV∈B
59 58 3adant3 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→F⁡V⋅MV∈B
60 6 a1i ⊢M∈LMod∧V≠W∧W∈B∧Y∈R→F=VXWY
61 60 fveq1d ⊢M∈LMod∧V≠W∧W∈B∧Y∈R→F⁡W=VXWY⁡W
62 simprl ⊢M∈LMod∧V≠W∧W∈B∧Y∈R→W∈B
63 simprr ⊢M∈LMod∧V≠W∧W∈B∧Y∈R→Y∈R
64 39 adantr ⊢M∈LMod∧V≠W∧W∈B∧Y∈R→V≠W
65 fvpr2g ⊢W∈B∧Y∈R∧V≠W→VXWY⁡W=Y
66 62 63 64 65 syl3anc ⊢M∈LMod∧V≠W∧W∈B∧Y∈R→VXWY⁡W=Y
67 61 66 eqtrd ⊢M∈LMod∧V≠W∧W∈B∧Y∈R→F⁡W=Y
68 67 oveq1d ⊢M∈LMod∧V≠W∧W∈B∧Y∈R→F⁡W⋅MW=Y⋅MW
69 7 adantr ⊢M∈LMod∧V≠W∧W∈B∧Y∈R→M∈LMod
70 1 2 55 3 lmodvscl ⊢M∈LMod∧Y∈R∧W∈B→Y⋅MW∈B
71 69 63 62 70 syl3anc ⊢M∈LMod∧V≠W∧W∈B∧Y∈R→Y⋅MW∈B
72 68 71 eqeltrd ⊢M∈LMod∧V≠W∧W∈B∧Y∈R→F⁡W⋅MW∈B
73 72 3adant2 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→F⁡W⋅MW∈B
74 fveq2 ⊢v=V→F⁡v=F⁡V
75 id ⊢v=V→v=V
76 74 75 oveq12d ⊢v=V→F⁡v⋅Mv=F⁡V⋅MV
77 fveq2 ⊢v=W→F⁡v=F⁡W
78 id ⊢v=W→v=W
79 77 78 oveq12d ⊢v=W→F⁡v⋅Mv=F⁡W⋅MW
80 1 5 76 79 gsumpr ⊢M∈CMnd∧V∈B∧W∈B∧V≠W∧F⁡V⋅MV∈B∧F⁡W⋅MW∈B→∑Mv∈VWF⁡v⋅Mv=F⁡V⋅MV+˙F⁡W⋅MW
81 38 44 59 73 80 syl112anc ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→∑Mv∈VWF⁡v⋅Mv=F⁡V⋅MV+˙F⁡W⋅MW
82 4 a1i ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→·˙=⋅M
83 82 eqcomd ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→⋅M=·˙
84 6 fveq1i ⊢F⁡V=VXWY⁡V
85 40 3ad2ant2 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→V∈B
86 simpr ⊢V∈B∧X∈R→X∈R
87 86 3ad2ant2 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→X∈R
88 39 3ad2ant1 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→V≠W
89 85 87 88 50 syl3anc ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→VXWY⁡V=X
90 84 89 eqtrid ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→F⁡V=X
91 eqidd ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→V=V
92 83 90 91 oveq123d ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→F⁡V⋅MV=X·˙V
93 6 fveq1i ⊢F⁡W=VXWY⁡W
94 41 3ad2ant3 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→W∈B
95 simpr ⊢W∈B∧Y∈R→Y∈R
96 95 3ad2ant3 ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→Y∈R
97 94 96 88 65 syl3anc ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→VXWY⁡W=Y
98 93 97 eqtrid ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→F⁡W=Y
99 eqidd ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→W=W
100 83 98 99 oveq123d ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→F⁡W⋅MW=Y·˙W
101 92 100 oveq12d ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→F⁡V⋅MV+˙F⁡W⋅MW=X·˙V+˙Y·˙W
102 35 81 101 3eqtrd ⊢M∈LMod∧V≠W∧V∈B∧X∈R∧W∈B∧Y∈R→FlinC⁡MVW=X·˙V+˙Y·˙W