Theorem zlmodzxz0

Description: The 0 of the ZZ-module ZZ X. ZZ . (Contributed by AV, 20-May-2019) (Revised by AV, 10-Jun-2019)

	Ref	Expression
Hypotheses	zlmodzxz.z	$$⊢Z={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
	zlmodzxz.o	$$⊢\underset{\dot{}}{0}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
Assertion	zlmodzxz0	$$⊢\underset{\dot{}}{0}=0_Z$$

Proof

Step	Hyp	Ref	Expression
1		zlmodzxz.z	$$⊢Z={\mathbb{Z}}_{\mathrm{ring}}\mathrm{freeLMod}\left\{0,1\right\}$$
2		zlmodzxz.o	$$⊢\underset{\dot{}}{0}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
3		c0ex	$$⊢0\in \mathrm{V}$$
4		1ex	$$⊢1\in \mathrm{V}$$
5		xpprsng	$$⊢\left(0\in \mathrm{V}\wedge 1\in \mathrm{V}\wedge 0\in \mathrm{V}\right)\to \left\{0,1\right\}\times \left\{0\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
6	3 4 3 5	mp3an	$$⊢\left\{0,1\right\}\times \left\{0\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
7		zringring	$$⊢{\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}$$
8		prex	$$⊢\left\{0,1\right\}\in \mathrm{V}$$
9		zring0	$$⊢0=0_{{\mathbb{Z}}_{\mathrm{ring}}}$$
10	1 9	frlm0	$$⊢\left({\mathbb{Z}}_{\mathrm{ring}}\in \mathrm{Ring}\wedge \left\{0,1\right\}\in \mathrm{V}\right)\to \left\{0,1\right\}\times \left\{0\right\}=0_Z$$
11	7 8 10	mp2an	$$⊢\left\{0,1\right\}\times \left\{0\right\}=0_Z$$
12	2 6 11	3eqtr2i	$$⊢\underset{\dot{}}{0}=0_Z$$