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