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 birani 
 |-  ( ( V e. B /\ X e. R ) -> V e. ( Base ` M ) )
27 1 eleq2i 
 |-  ( W e. B <-> W e. ( Base ` M ) )
28 27 birani 
 |-  ( ( W e. B /\ Y e. R ) -> W e. ( Base ` M ) )
29 prelpwi 
 |-  ( ( V e. ( Base ` M ) /\ W e. ( Base ` M ) ) -> { V , W } e. ~P ( Base ` M ) )
30 26 28 29 syl2an 
 |-  ( ( ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> { V , W } e. ~P ( Base ` M ) )
31 30 3adant1 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> { V , W } e. ~P ( Base ` M ) )
32 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 ) ) ) )
33 8 24 31 32 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 ) ) ) )
34 lmodcmn 
 |-  ( M e. LMod -> M e. CMnd )
35 34 adantr 
 |-  ( ( M e. LMod /\ V =/= W ) -> M e. CMnd )
36 35 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> M e. CMnd )
37 simpr 
 |-  ( ( M e. LMod /\ V =/= W ) -> V =/= W )
38 simpl 
 |-  ( ( V e. B /\ X e. R ) -> V e. B )
39 simpl 
 |-  ( ( W e. B /\ Y e. R ) -> W e. B )
40 37 38 39 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 ) )
41 3anrot 
 |-  ( ( V =/= W /\ V e. B /\ W e. B ) <-> ( V e. B /\ W e. B /\ V =/= W ) )
42 40 41 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 ) )
43 6 a1i 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) ) -> F = { <. V , X >. , <. W , Y >. } )
44 43 fveq1d 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) ) -> ( F ` V ) = ( { <. V , X >. , <. W , Y >. } ` V ) )
45 simprl 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) ) -> V e. B )
46 simprr 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) ) -> X e. R )
47 37 adantr 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) ) -> V =/= W )
48 fvpr1g 
 |-  ( ( V e. B /\ X e. R /\ V =/= W ) -> ( { <. V , X >. , <. W , Y >. } ` V ) = X )
49 45 46 47 48 syl3anc 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) ) -> ( { <. V , X >. , <. W , Y >. } ` V ) = X )
50 44 49 eqtrd 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) ) -> ( F ` V ) = X )
51 50 oveq1d 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) ) -> ( ( F ` V ) ( .s ` M ) V ) = ( X ( .s ` M ) V ) )
52 7 adantr 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) ) -> M e. LMod )
53 eqid 
 |-  ( .s ` M ) = ( .s ` M )
54 1 2 53 3 lmodvscl 
 |-  ( ( M e. LMod /\ X e. R /\ V e. B ) -> ( X ( .s ` M ) V ) e. B )
55 52 46 45 54 syl3anc 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) ) -> ( X ( .s ` M ) V ) e. B )
56 51 55 eqeltrd 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) ) -> ( ( F ` V ) ( .s ` M ) V ) e. B )
57 56 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 )
58 6 a1i 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( W e. B /\ Y e. R ) ) -> F = { <. V , X >. , <. W , Y >. } )
59 58 fveq1d 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( W e. B /\ Y e. R ) ) -> ( F ` W ) = ( { <. V , X >. , <. W , Y >. } ` W ) )
60 simprl 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( W e. B /\ Y e. R ) ) -> W e. B )
61 simprr 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( W e. B /\ Y e. R ) ) -> Y e. R )
62 37 adantr 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( W e. B /\ Y e. R ) ) -> V =/= W )
63 fvpr2g 
 |-  ( ( W e. B /\ Y e. R /\ V =/= W ) -> ( { <. V , X >. , <. W , Y >. } ` W ) = Y )
64 60 61 62 63 syl3anc 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( W e. B /\ Y e. R ) ) -> ( { <. V , X >. , <. W , Y >. } ` W ) = Y )
65 59 64 eqtrd 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( W e. B /\ Y e. R ) ) -> ( F ` W ) = Y )
66 65 oveq1d 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( W e. B /\ Y e. R ) ) -> ( ( F ` W ) ( .s ` M ) W ) = ( Y ( .s ` M ) W ) )
67 7 adantr 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( W e. B /\ Y e. R ) ) -> M e. LMod )
68 1 2 53 3 lmodvscl 
 |-  ( ( M e. LMod /\ Y e. R /\ W e. B ) -> ( Y ( .s ` M ) W ) e. B )
69 67 61 60 68 syl3anc 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( W e. B /\ Y e. R ) ) -> ( Y ( .s ` M ) W ) e. B )
70 66 69 eqeltrd 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( W e. B /\ Y e. R ) ) -> ( ( F ` W ) ( .s ` M ) W ) e. B )
71 70 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 )
72 fveq2 
 |-  ( v = V -> ( F ` v ) = ( F ` V ) )
73 id 
 |-  ( v = V -> v = V )
74 72 73 oveq12d 
 |-  ( v = V -> ( ( F ` v ) ( .s ` M ) v ) = ( ( F ` V ) ( .s ` M ) V ) )
75 fveq2 
 |-  ( v = W -> ( F ` v ) = ( F ` W ) )
76 id 
 |-  ( v = W -> v = W )
77 75 76 oveq12d 
 |-  ( v = W -> ( ( F ` v ) ( .s ` M ) v ) = ( ( F ` W ) ( .s ` M ) W ) )
78 1 5 74 77 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 ) ) )
79 36 42 57 71 78 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 ) ) )
80 4 a1i 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> .x. = ( .s ` M ) )
81 80 eqcomd 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> ( .s ` M ) = .x. )
82 6 fveq1i 
 |-  ( F ` V ) = ( { <. V , X >. , <. W , Y >. } ` V )
83 38 3ad2ant2 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> V e. B )
84 simpr 
 |-  ( ( V e. B /\ X e. R ) -> X e. R )
85 84 3ad2ant2 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> X e. R )
86 37 3ad2ant1 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> V =/= W )
87 83 85 86 48 syl3anc 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> ( { <. V , X >. , <. W , Y >. } ` V ) = X )
88 82 87 eqtrid 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> ( F ` V ) = X )
89 eqidd 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> V = V )
90 81 88 89 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 ) )
91 6 fveq1i 
 |-  ( F ` W ) = ( { <. V , X >. , <. W , Y >. } ` W )
92 39 3ad2ant3 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> W e. B )
93 simpr 
 |-  ( ( W e. B /\ Y e. R ) -> Y e. R )
94 93 3ad2ant3 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> Y e. R )
95 92 94 86 63 syl3anc 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> ( { <. V , X >. , <. W , Y >. } ` W ) = Y )
96 91 95 eqtrid 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> ( F ` W ) = Y )
97 eqidd 
 |-  ( ( ( M e. LMod /\ V =/= W ) /\ ( V e. B /\ X e. R ) /\ ( W e. B /\ Y e. R ) ) -> W = W )
98 81 96 97 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 ) )
99 90 98 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 ) ) )
100 33 79 99 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 ) ) )