Theorem zlmodzxzldeplem

Description: A and B are not equal. (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\}$$
Assertion	zlmodzxzldeplem	$$⊢A\ne B$$

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		opex	$$⊢⟨0,3⟩\in \mathrm{V}$$
5		opex	$$⊢⟨1,6⟩\in \mathrm{V}$$
6	4 5	pm3.2i	$$⊢\left(⟨0,3⟩\in \mathrm{V}\wedge ⟨1,6⟩\in \mathrm{V}\right)$$
7		opex	$$⊢⟨0,2⟩\in \mathrm{V}$$
8		opex	$$⊢⟨1,4⟩\in \mathrm{V}$$
9	7 8	pm3.2i	$$⊢\left(⟨0,2⟩\in \mathrm{V}\wedge ⟨1,4⟩\in \mathrm{V}\right)$$
10	6 9	pm3.2i	$$⊢\left(\left(⟨0,3⟩\in \mathrm{V}\wedge ⟨1,6⟩\in \mathrm{V}\right)\wedge \left(⟨0,2⟩\in \mathrm{V}\wedge ⟨1,4⟩\in \mathrm{V}\right)\right)$$
11		2re	$$⊢2\in ℝ$$
12		2lt3	$$⊢2<3$$
13	11 12	gtneii	$$⊢3\ne 2$$
14	13	olci	$$⊢\left(0\ne 0\vee 3\ne 2\right)$$
15		c0ex	$$⊢0\in \mathrm{V}$$
16		3ex	$$⊢3\in \mathrm{V}$$
17	15 16	opthne	$$⊢⟨0,3⟩\ne ⟨0,2⟩\leftrightarrow \left(0\ne 0\vee 3\ne 2\right)$$
18	14 17	mpbir	$$⊢⟨0,3⟩\ne ⟨0,2⟩$$
19		0ne1	$$⊢0\ne 1$$
20	19	orci	$$⊢\left(0\ne 1\vee 3\ne 4\right)$$
21	15 16	opthne	$$⊢⟨0,3⟩\ne ⟨1,4⟩\leftrightarrow \left(0\ne 1\vee 3\ne 4\right)$$
22	20 21	mpbir	$$⊢⟨0,3⟩\ne ⟨1,4⟩$$
23	18 22	pm3.2i	$$⊢\left(⟨0,3⟩\ne ⟨0,2⟩\wedge ⟨0,3⟩\ne ⟨1,4⟩\right)$$
24	23	orci	$$⊢\left(\left(⟨0,3⟩\ne ⟨0,2⟩\wedge ⟨0,3⟩\ne ⟨1,4⟩\right)\vee \left(⟨1,6⟩\ne ⟨0,2⟩\wedge ⟨1,6⟩\ne ⟨1,4⟩\right)\right)$$
25		prneimg	$$⊢\left(\left(⟨0,3⟩\in \mathrm{V}\wedge ⟨1,6⟩\in \mathrm{V}\right)\wedge \left(⟨0,2⟩\in \mathrm{V}\wedge ⟨1,4⟩\in \mathrm{V}\right)\right)\to \left(\left(\left(⟨0,3⟩\ne ⟨0,2⟩\wedge ⟨0,3⟩\ne ⟨1,4⟩\right)\vee \left(⟨1,6⟩\ne ⟨0,2⟩\wedge ⟨1,6⟩\ne ⟨1,4⟩\right)\right)\to \left\{⟨0,3⟩,⟨1,6⟩\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}\right)$$
26	10 24 25	mp2	$$⊢\left\{⟨0,3⟩,⟨1,6⟩\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}$$
27	2 3	neeq12i	$$⊢A\ne B\leftrightarrow \left\{⟨0,3⟩,⟨1,6⟩\right\}\ne \left\{⟨0,2⟩,⟨1,4⟩\right\}$$
28	26 27	mpbir	$$⊢A\ne B$$