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={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
	zlmodzxzldep.a	$$⊢A=\left\{⟨0,3⟩,⟨1,6⟩\right\}$$
	zlmodzxzldep.b	$$⊢B=\left\{⟨0,2⟩,⟨1,4⟩\right\}$$
	zlmodzxzldeplem.f	$$⊢F=\left\{⟨A,2⟩,⟨B,-3⟩\right\}$$
Assertion	zlmodzxzldeplem4	$$⊢\exists y\in \left\{A,B\right\}F\left(y\right)\ne 0$$

Proof

Step	Hyp	Ref	Expression
1		zlmodzxzldep.z	$$⊢Z={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
2		zlmodzxzldep.a	$$⊢A=\left\{⟨0,3⟩,⟨1,6⟩\right\}$$
3		zlmodzxzldep.b	$$⊢B=\left\{⟨0,2⟩,⟨1,4⟩\right\}$$
4		zlmodzxzldeplem.f	$$⊢F=\left\{⟨A,2⟩,⟨B,-3⟩\right\}$$
5		prex	$$⊢\left\{⟨0,3⟩,⟨1,6⟩\right\}\in \mathrm{V}$$
6	2 5	eqeltri	$$⊢A\in \mathrm{V}$$
7		prex	$$⊢\left\{⟨0,2⟩,⟨1,4⟩\right\}\in \mathrm{V}$$
8	3 7	eqeltri	$$⊢B\in \mathrm{V}$$
9		2ne0	$$⊢2\ne 0$$
10	4	fveq1i	$$⊢F\left(A\right)=\left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(A\right)$$
11	1 2 3	zlmodzxzldeplem	$$⊢A\ne B$$
12		2ex	$$⊢2\in \mathrm{V}$$
13	6 12	fvpr1	$$⊢A\ne B\to \left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(A\right)=2$$
14	11 13	mp1i	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left\{⟨A,2⟩,⟨B,-3⟩\right\}\left(A\right)=2$$
15	10 14	syl5eq	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to F\left(A\right)=2$$
16	15	neeq1d	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(F\left(A\right)\ne 0\leftrightarrow 2\ne 0\right)$$
17	9 16	mpbiri	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to F\left(A\right)\ne 0$$
18	17	orcd	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(F\left(A\right)\ne 0\vee F\left(B\right)\ne 0\right)$$
19		fveq2	$$⊢y=A\to F\left(y\right)=F\left(A\right)$$
20	19	neeq1d	$$⊢y=A\to \left(F\left(y\right)\ne 0\leftrightarrow F\left(A\right)\ne 0\right)$$
21		fveq2	$$⊢y=B\to F\left(y\right)=F\left(B\right)$$
22	21	neeq1d	$$⊢y=B\to \left(F\left(y\right)\ne 0\leftrightarrow F\left(B\right)\ne 0\right)$$
23	20 22	rexprg	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \left(\exists y\in \left\{A,B\right\}F\left(y\right)\ne 0\leftrightarrow \left(F\left(A\right)\ne 0\vee F\left(B\right)\ne 0\right)\right)$$
24	18 23	mpbird	$$⊢\left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)\to \exists y\in \left\{A,B\right\}F\left(y\right)\ne 0$$
25	6 8 24	mp2an	$$⊢\exists y\in \left\{A,B\right\}F\left(y\right)\ne 0$$