Metamath Proof Explorer

Theorem ldepsnlinclem2

Description: Lemma 2 for ldepsnlinc . (Contributed by AV, 25-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 >. }
Assertion ldepsnlinclem2 
|- ( F e. ( ( Base ` ZZring ) ^m { A } ) -> ( F ( linC ` Z ) { A } ) =/= B )

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 elmapi 
 |-  ( F e. ( ( Base ` ZZring ) ^m { A } ) -> F : { A } --> ( Base ` ZZring ) )
5 prex 
 |-  { <. 0 , 3 >. , <. 1 , 6 >. } e. _V
6 2 5 eqeltri 
 |-  A e. _V
7 6 fsn2 
 |-  ( F : { A } --> ( Base ` ZZring ) <-> ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) )
8 oveq1 
 |-  ( F = { <. A , ( F ` A ) >. } -> ( F ( linC ` Z ) { A } ) = ( { <. A , ( F ` A ) >. } ( linC ` Z ) { A } ) )
9 8 adantl 
 |-  ( ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) -> ( F ( linC ` Z ) { A } ) = ( { <. A , ( F ` A ) >. } ( linC ` Z ) { A } ) )
10 1 zlmodzxzlmod 
 |-  ( Z e. LMod /\ ZZring = ( Scalar ` Z ) )
11 10 simpli 
 |-  Z e. LMod
12 11 a1i 
 |-  ( ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) -> Z e. LMod )
13 3z 
 |-  3 e. ZZ
14 6nn 
 |-  6 e. NN
15 14 nnzi 
 |-  6 e. ZZ
16 1 zlmodzxzel 
 |-  ( ( 3 e. ZZ /\ 6 e. ZZ ) -> { <. 0 , 3 >. , <. 1 , 6 >. } e. ( Base ` Z ) )
17 13 15 16 mp2an 
 |-  { <. 0 , 3 >. , <. 1 , 6 >. } e. ( Base ` Z )
18 2 17 eqeltri 
 |-  A e. ( Base ` Z )
19 18 a1i 
 |-  ( ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) -> A e. ( Base ` Z ) )
20 simpl 
 |-  ( ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) -> ( F ` A ) e. ( Base ` ZZring ) )
21 eqid 
 |-  ( Base ` Z ) = ( Base ` Z )
22 10 simpri 
 |-  ZZring = ( Scalar ` Z )
23 eqid 
 |-  ( Base ` ZZring ) = ( Base ` ZZring )
24 eqid 
 |-  ( .s ` Z ) = ( .s ` Z )
25 21 22 23 24 lincvalsng 
 |-  ( ( Z e. LMod /\ A e. ( Base ` Z ) /\ ( F ` A ) e. ( Base ` ZZring ) ) -> ( { <. A , ( F ` A ) >. } ( linC ` Z ) { A } ) = ( ( F ` A ) ( .s ` Z ) A ) )
26 12 19 20 25 syl3anc 
 |-  ( ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) -> ( { <. A , ( F ` A ) >. } ( linC ` Z ) { A } ) = ( ( F ` A ) ( .s ` Z ) A ) )
27 9 26 eqtrd 
 |-  ( ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) -> ( F ( linC ` Z ) { A } ) = ( ( F ` A ) ( .s ` Z ) A ) )
28 eqid 
 |-  { <. 0 , 0 >. , <. 1 , 0 >. } = { <. 0 , 0 >. , <. 1 , 0 >. }
29 eqid 
 |-  ( -g ` Z ) = ( -g ` Z )
30 1 28 24 29 2 3 zlmodzxznm 
 |-  A. i e. ZZ ( ( i ( .s ` Z ) A ) =/= B /\ ( i ( .s ` Z ) B ) =/= A )
31 r19.26 
 |-  ( A. i e. ZZ ( ( i ( .s ` Z ) A ) =/= B /\ ( i ( .s ` Z ) B ) =/= A ) <-> ( A. i e. ZZ ( i ( .s ` Z ) A ) =/= B /\ A. i e. ZZ ( i ( .s ` Z ) B ) =/= A ) )
32 oveq1 
 |-  ( i = ( F ` A ) -> ( i ( .s ` Z ) A ) = ( ( F ` A ) ( .s ` Z ) A ) )
33 32 neeq1d 
 |-  ( i = ( F ` A ) -> ( ( i ( .s ` Z ) A ) =/= B <-> ( ( F ` A ) ( .s ` Z ) A ) =/= B ) )
34 33 rspcv 
 |-  ( ( F ` A ) e. ZZ -> ( A. i e. ZZ ( i ( .s ` Z ) A ) =/= B -> ( ( F ` A ) ( .s ` Z ) A ) =/= B ) )
35 zringbas 
 |-  ZZ = ( Base ` ZZring )
36 35 eqcomi 
 |-  ( Base ` ZZring ) = ZZ
37 36 eleq2i 
 |-  ( ( F ` A ) e. ( Base ` ZZring ) <-> ( F ` A ) e. ZZ )
38 37 biimpi 
 |-  ( ( F ` A ) e. ( Base ` ZZring ) -> ( F ` A ) e. ZZ )
39 38 adantr 
 |-  ( ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) -> ( F ` A ) e. ZZ )
40 34 39 syl11 
 |-  ( A. i e. ZZ ( i ( .s ` Z ) A ) =/= B -> ( ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) -> ( ( F ` A ) ( .s ` Z ) A ) =/= B ) )
41 40 adantr 
 |-  ( ( A. i e. ZZ ( i ( .s ` Z ) A ) =/= B /\ A. i e. ZZ ( i ( .s ` Z ) B ) =/= A ) -> ( ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) -> ( ( F ` A ) ( .s ` Z ) A ) =/= B ) )
42 31 41 sylbi 
 |-  ( A. i e. ZZ ( ( i ( .s ` Z ) A ) =/= B /\ ( i ( .s ` Z ) B ) =/= A ) -> ( ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) -> ( ( F ` A ) ( .s ` Z ) A ) =/= B ) )
43 30 42 ax-mp 
 |-  ( ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) -> ( ( F ` A ) ( .s ` Z ) A ) =/= B )
44 27 43 eqnetrd 
 |-  ( ( ( F ` A ) e. ( Base ` ZZring ) /\ F = { <. A , ( F ` A ) >. } ) -> ( F ( linC ` Z ) { A } ) =/= B )
45 7 44 sylbi 
 |-  ( F : { A } --> ( Base ` ZZring ) -> ( F ( linC ` Z ) { A } ) =/= B )
46 4 45 syl 
 |-  ( F e. ( ( Base ` ZZring ) ^m { A } ) -> ( F ( linC ` Z ) { A } ) =/= B )