Metamath Proof Explorer


Theorem zlmodzxzldeplem3

Description: Lemma 3 for zlmodzxzldep . (Contributed by AV, 24-May-2019) (Revised by AV, 10-Jun-2019)

Ref Expression
Hypotheses zlmodzxzldep.z
|- Z = ( ZZring freeLMod { 0 , 1 } )
zlmodzxzldep.a
|- A = { <. 0 , 3 >. , <. 1 , 6 >. }
zlmodzxzldep.b
|- B = { <. 0 , 2 >. , <. 1 , 4 >. }
zlmodzxzldeplem.f
|- F = { <. A , 2 >. , <. B , -u 3 >. }
Assertion zlmodzxzldeplem3
|- ( F ( linC ` Z ) { A , B } ) = ( 0g ` Z )

Proof

Step Hyp Ref Expression
1 zlmodzxzldep.z
 |-  Z = ( ZZring freeLMod { 0 , 1 } )
2 zlmodzxzldep.a
 |-  A = { <. 0 , 3 >. , <. 1 , 6 >. }
3 zlmodzxzldep.b
 |-  B = { <. 0 , 2 >. , <. 1 , 4 >. }
4 zlmodzxzldeplem.f
 |-  F = { <. A , 2 >. , <. B , -u 3 >. }
5 ovex
 |-  ( ZZring freeLMod { 0 , 1 } ) e. _V
6 1 5 eqeltri
 |-  Z e. _V
7 1 2 3 4 zlmodzxzldeplem1
 |-  F e. ( ZZ ^m { A , B } )
8 1 zlmodzxzlmod
 |-  ( Z e. LMod /\ ZZring = ( Scalar ` Z ) )
9 simpr
 |-  ( ( Z e. LMod /\ ZZring = ( Scalar ` Z ) ) -> ZZring = ( Scalar ` Z ) )
10 9 eqcomd
 |-  ( ( Z e. LMod /\ ZZring = ( Scalar ` Z ) ) -> ( Scalar ` Z ) = ZZring )
11 8 10 ax-mp
 |-  ( Scalar ` Z ) = ZZring
12 11 fveq2i
 |-  ( Base ` ( Scalar ` Z ) ) = ( Base ` ZZring )
13 zringbas
 |-  ZZ = ( Base ` ZZring )
14 13 eqcomi
 |-  ( Base ` ZZring ) = ZZ
15 12 14 eqtri
 |-  ( Base ` ( Scalar ` Z ) ) = ZZ
16 15 oveq1i
 |-  ( ( Base ` ( Scalar ` Z ) ) ^m { A , B } ) = ( ZZ ^m { A , B } )
17 7 16 eleqtrri
 |-  F e. ( ( Base ` ( Scalar ` Z ) ) ^m { A , B } )
18 3z
 |-  3 e. ZZ
19 6nn
 |-  6 e. NN
20 19 nnzi
 |-  6 e. ZZ
21 1 zlmodzxzel
 |-  ( ( 3 e. ZZ /\ 6 e. ZZ ) -> { <. 0 , 3 >. , <. 1 , 6 >. } e. ( Base ` Z ) )
22 18 20 21 mp2an
 |-  { <. 0 , 3 >. , <. 1 , 6 >. } e. ( Base ` Z )
23 2z
 |-  2 e. ZZ
24 4z
 |-  4 e. ZZ
25 1 zlmodzxzel
 |-  ( ( 2 e. ZZ /\ 4 e. ZZ ) -> { <. 0 , 2 >. , <. 1 , 4 >. } e. ( Base ` Z ) )
26 23 24 25 mp2an
 |-  { <. 0 , 2 >. , <. 1 , 4 >. } e. ( Base ` Z )
27 2 eleq1i
 |-  ( A e. ( Base ` Z ) <-> { <. 0 , 3 >. , <. 1 , 6 >. } e. ( Base ` Z ) )
28 3 eleq1i
 |-  ( B e. ( Base ` Z ) <-> { <. 0 , 2 >. , <. 1 , 4 >. } e. ( Base ` Z ) )
29 27 28 anbi12i
 |-  ( ( A e. ( Base ` Z ) /\ B e. ( Base ` Z ) ) <-> ( { <. 0 , 3 >. , <. 1 , 6 >. } e. ( Base ` Z ) /\ { <. 0 , 2 >. , <. 1 , 4 >. } e. ( Base ` Z ) ) )
30 22 26 29 mpbir2an
 |-  ( A e. ( Base ` Z ) /\ B e. ( Base ` Z ) )
31 prelpwi
 |-  ( ( A e. ( Base ` Z ) /\ B e. ( Base ` Z ) ) -> { A , B } e. ~P ( Base ` Z ) )
32 30 31 ax-mp
 |-  { A , B } e. ~P ( Base ` Z )
33 lincval
 |-  ( ( Z e. _V /\ F e. ( ( Base ` ( Scalar ` Z ) ) ^m { A , B } ) /\ { A , B } e. ~P ( Base ` Z ) ) -> ( F ( linC ` Z ) { A , B } ) = ( Z gsum ( x e. { A , B } |-> ( ( F ` x ) ( .s ` Z ) x ) ) ) )
34 6 17 32 33 mp3an
 |-  ( F ( linC ` Z ) { A , B } ) = ( Z gsum ( x e. { A , B } |-> ( ( F ` x ) ( .s ` Z ) x ) ) )
35 lmodcmn
 |-  ( Z e. LMod -> Z e. CMnd )
36 35 adantr
 |-  ( ( Z e. LMod /\ ZZring = ( Scalar ` Z ) ) -> Z e. CMnd )
37 8 36 ax-mp
 |-  Z e. CMnd
38 prex
 |-  { <. 0 , 3 >. , <. 1 , 6 >. } e. _V
39 2 38 eqeltri
 |-  A e. _V
40 prex
 |-  { <. 0 , 2 >. , <. 1 , 4 >. } e. _V
41 3 40 eqeltri
 |-  B e. _V
42 1 2 3 zlmodzxzldeplem
 |-  A =/= B
43 39 41 42 3pm3.2i
 |-  ( A e. _V /\ B e. _V /\ A =/= B )
44 8 simpli
 |-  Z e. LMod
45 elmapi
 |-  ( F e. ( ZZ ^m { A , B } ) -> F : { A , B } --> ZZ )
46 39 prid1
 |-  A e. { A , B }
47 ffvelrn
 |-  ( ( F : { A , B } --> ZZ /\ A e. { A , B } ) -> ( F ` A ) e. ZZ )
48 46 47 mpan2
 |-  ( F : { A , B } --> ZZ -> ( F ` A ) e. ZZ )
49 7 45 48 mp2b
 |-  ( F ` A ) e. ZZ
50 8 9 ax-mp
 |-  ZZring = ( Scalar ` Z )
51 50 eqcomi
 |-  ( Scalar ` Z ) = ZZring
52 51 fveq2i
 |-  ( Base ` ( Scalar ` Z ) ) = ( Base ` ZZring )
53 52 14 eqtri
 |-  ( Base ` ( Scalar ` Z ) ) = ZZ
54 49 53 eleqtrri
 |-  ( F ` A ) e. ( Base ` ( Scalar ` Z ) )
55 2 22 eqeltri
 |-  A e. ( Base ` Z )
56 eqid
 |-  ( Base ` Z ) = ( Base ` Z )
57 eqid
 |-  ( Scalar ` Z ) = ( Scalar ` Z )
58 eqid
 |-  ( .s ` Z ) = ( .s ` Z )
59 eqid
 |-  ( Base ` ( Scalar ` Z ) ) = ( Base ` ( Scalar ` Z ) )
60 56 57 58 59 lmodvscl
 |-  ( ( Z e. LMod /\ ( F ` A ) e. ( Base ` ( Scalar ` Z ) ) /\ A e. ( Base ` Z ) ) -> ( ( F ` A ) ( .s ` Z ) A ) e. ( Base ` Z ) )
61 44 54 55 60 mp3an
 |-  ( ( F ` A ) ( .s ` Z ) A ) e. ( Base ` Z )
62 41 prid2
 |-  B e. { A , B }
63 ffvelrn
 |-  ( ( F : { A , B } --> ZZ /\ B e. { A , B } ) -> ( F ` B ) e. ZZ )
64 62 63 mpan2
 |-  ( F : { A , B } --> ZZ -> ( F ` B ) e. ZZ )
65 7 45 64 mp2b
 |-  ( F ` B ) e. ZZ
66 65 53 eleqtrri
 |-  ( F ` B ) e. ( Base ` ( Scalar ` Z ) )
67 3 26 eqeltri
 |-  B e. ( Base ` Z )
68 56 57 58 59 lmodvscl
 |-  ( ( Z e. LMod /\ ( F ` B ) e. ( Base ` ( Scalar ` Z ) ) /\ B e. ( Base ` Z ) ) -> ( ( F ` B ) ( .s ` Z ) B ) e. ( Base ` Z ) )
69 44 66 67 68 mp3an
 |-  ( ( F ` B ) ( .s ` Z ) B ) e. ( Base ` Z )
70 61 69 pm3.2i
 |-  ( ( ( F ` A ) ( .s ` Z ) A ) e. ( Base ` Z ) /\ ( ( F ` B ) ( .s ` Z ) B ) e. ( Base ` Z ) )
71 eqid
 |-  ( +g ` Z ) = ( +g ` Z )
72 fveq2
 |-  ( x = A -> ( F ` x ) = ( F ` A ) )
73 id
 |-  ( x = A -> x = A )
74 72 73 oveq12d
 |-  ( x = A -> ( ( F ` x ) ( .s ` Z ) x ) = ( ( F ` A ) ( .s ` Z ) A ) )
75 fveq2
 |-  ( x = B -> ( F ` x ) = ( F ` B ) )
76 id
 |-  ( x = B -> x = B )
77 75 76 oveq12d
 |-  ( x = B -> ( ( F ` x ) ( .s ` Z ) x ) = ( ( F ` B ) ( .s ` Z ) B ) )
78 56 71 74 77 gsumpr
 |-  ( ( Z e. CMnd /\ ( A e. _V /\ B e. _V /\ A =/= B ) /\ ( ( ( F ` A ) ( .s ` Z ) A ) e. ( Base ` Z ) /\ ( ( F ` B ) ( .s ` Z ) B ) e. ( Base ` Z ) ) ) -> ( Z gsum ( x e. { A , B } |-> ( ( F ` x ) ( .s ` Z ) x ) ) ) = ( ( ( F ` A ) ( .s ` Z ) A ) ( +g ` Z ) ( ( F ` B ) ( .s ` Z ) B ) ) )
79 37 43 70 78 mp3an
 |-  ( Z gsum ( x e. { A , B } |-> ( ( F ` x ) ( .s ` Z ) x ) ) ) = ( ( ( F ` A ) ( .s ` Z ) A ) ( +g ` Z ) ( ( F ` B ) ( .s ` Z ) B ) )
80 4 fveq1i
 |-  ( F ` A ) = ( { <. A , 2 >. , <. B , -u 3 >. } ` A )
81 2ex
 |-  2 e. _V
82 39 81 fvpr1
 |-  ( A =/= B -> ( { <. A , 2 >. , <. B , -u 3 >. } ` A ) = 2 )
83 42 82 ax-mp
 |-  ( { <. A , 2 >. , <. B , -u 3 >. } ` A ) = 2
84 80 83 eqtri
 |-  ( F ` A ) = 2
85 84 oveq1i
 |-  ( ( F ` A ) ( .s ` Z ) A ) = ( 2 ( .s ` Z ) A )
86 4 fveq1i
 |-  ( F ` B ) = ( { <. A , 2 >. , <. B , -u 3 >. } ` B )
87 negex
 |-  -u 3 e. _V
88 41 87 fvpr2
 |-  ( A =/= B -> ( { <. A , 2 >. , <. B , -u 3 >. } ` B ) = -u 3 )
89 42 88 ax-mp
 |-  ( { <. A , 2 >. , <. B , -u 3 >. } ` B ) = -u 3
90 86 89 eqtri
 |-  ( F ` B ) = -u 3
91 90 oveq1i
 |-  ( ( F ` B ) ( .s ` Z ) B ) = ( -u 3 ( .s ` Z ) B )
92 85 91 oveq12i
 |-  ( ( ( F ` A ) ( .s ` Z ) A ) ( +g ` Z ) ( ( F ` B ) ( .s ` Z ) B ) ) = ( ( 2 ( .s ` Z ) A ) ( +g ` Z ) ( -u 3 ( .s ` Z ) B ) )
93 eqid
 |-  { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. }
94 1 93 zlmodzxz0
 |-  { <. 0 , 0 >. , <. 1 , 0 >. } = ( 0g ` Z )
95 94 eqcomi
 |-  ( 0g ` Z ) = { <. 0 , 0 >. , <. 1 , 0 >. }
96 1 2 3 95 71 58 zlmodzxzequap
 |-  ( ( 2 ( .s ` Z ) A ) ( +g ` Z ) ( -u 3 ( .s ` Z ) B ) ) = ( 0g ` Z )
97 92 96 eqtri
 |-  ( ( ( F ` A ) ( .s ` Z ) A ) ( +g ` Z ) ( ( F ` B ) ( .s ` Z ) B ) ) = ( 0g ` Z )
98 34 79 97 3eqtri
 |-  ( F ( linC ` Z ) { A , B } ) = ( 0g ` Z )