Metamath Proof Explorer

Theorem zlmodzxzldeplem4

Description: Lemma 4 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 zlmodzxzldeplem4 
|- E. y e. { A , B } ( F ` y ) =/= 0

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 prex 
 |-  { <. 0 , 3 >. , <. 1 , 6 >. } e. _V
6 2 5 eqeltri 
 |-  A e. _V
7 prex 
 |-  { <. 0 , 2 >. , <. 1 , 4 >. } e. _V
8 3 7 eqeltri 
 |-  B e. _V
9 2ne0 
 |-  2 =/= 0
10 4 fveq1i 
 |-  ( F ` A ) = ( { <. A , 2 >. , <. B , -u 3 >. } ` A )
11 1 2 3 zlmodzxzldeplem 
 |-  A =/= B
12 2ex 
 |-  2 e. _V
13 6 12 fvpr1 
 |-  ( A =/= B -> ( { <. A , 2 >. , <. B , -u 3 >. } ` A ) = 2 )
14 11 13 mp1i 
 |-  ( ( A e. _V /\ B e. _V ) -> ( { <. A , 2 >. , <. B , -u 3 >. } ` A ) = 2 )
15 10 14 eqtrid 
 |-  ( ( A e. _V /\ B e. _V ) -> ( F ` A ) = 2 )
16 15 neeq1d 
 |-  ( ( A e. _V /\ B e. _V ) -> ( ( F ` A ) =/= 0 <-> 2 =/= 0 ) )
17 9 16 mpbiri 
 |-  ( ( A e. _V /\ B e. _V ) -> ( F ` A ) =/= 0 )
18 17 orcd 
 |-  ( ( A e. _V /\ B e. _V ) -> ( ( F ` A ) =/= 0 \/ ( F ` B ) =/= 0 ) )
19 fveq2 
 |-  ( y = A -> ( F ` y ) = ( F ` A ) )
20 19 neeq1d 
 |-  ( y = A -> ( ( F ` y ) =/= 0 <-> ( F ` A ) =/= 0 ) )
21 fveq2 
 |-  ( y = B -> ( F ` y ) = ( F ` B ) )
22 21 neeq1d 
 |-  ( y = B -> ( ( F ` y ) =/= 0 <-> ( F ` B ) =/= 0 ) )
23 20 22 rexprg 
 |-  ( ( A e. _V /\ B e. _V ) -> ( E. y e. { A , B } ( F ` y ) =/= 0 <-> ( ( F ` A ) =/= 0 \/ ( F ` B ) =/= 0 ) ) )
24 18 23 mpbird 
 |-  ( ( A e. _V /\ B e. _V ) -> E. y e. { A , B } ( F ` y ) =/= 0 )
25 6 8 24 mp2an 
 |-  E. y e. { A , B } ( F ` y ) =/= 0