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 syl5eq
 |-  ( ( 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