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 ffvelcdm 
 |-  ( ( 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 ffvelcdm 
 |-  ( ( 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 )