Metamath Proof Explorer

Theorem ldepsnlinclem1

Description: Lemma 1 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 ldepsnlinclem1 
|- ( F e. ( ( Base ` ZZring ) ^m { B } ) -> ( F ( linC ` Z ) { B } ) =/= A )

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