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 = ring freeLMod 0 1
zlmodzxzldep.a A = 0 3 1 6
zlmodzxzldep.b B = 0 2 1 4
zlmodzxzldeplem.f F = A 2 B 3
Assertion zlmodzxzldeplem4 y A B F y 0

Proof

Step Hyp Ref Expression
1 zlmodzxzldep.z Z = ring 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 3
5 prex 0 3 1 6 V
6 2 5 eqeltri A V
7 prex 0 2 1 4 V
8 3 7 eqeltri B V
9 2ne0 2 0
10 4 fveq1i F A = A 2 B 3 A
11 1 2 3 zlmodzxzldeplem A B
12 2ex 2 V
13 6 12 fvpr1 A B A 2 B 3 A = 2
14 11 13 mp1i A V B V A 2 B 3 A = 2
15 10 14 syl5eq A V B V F A = 2
16 15 neeq1d A V B V F A 0 2 0
17 9 16 mpbiri A V B V F A 0
18 17 orcd A V B 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 V B V y A B F y 0 F A 0 F B 0
24 18 23 mpbird A V B V y A B F y 0
25 6 8 24 mp2an y A B F y 0