Theorem zrdivrng

Description: The zero ring is not a division ring. (Contributed by FL, 24-Jan-2010) (Proof shortened by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	zrdivrng.1	$$⊢A\in \mathrm{V}$$
Assertion	zrdivrng	$$⊢\neg ⟨\left\{⟨⟨A,A⟩,A⟩\right\},\left\{⟨⟨A,A⟩,A⟩\right\}⟩\in \mathrm{DivRingOps}$$

Proof

Step	Hyp	Ref	Expression
1		zrdivrng.1	$$⊢A\in \mathrm{V}$$
2		0ngrp	$$⊢\neg \varnothing \in \mathrm{GrpOp}$$
3		opex	$$⊢⟨A,A⟩\in \mathrm{V}$$
4	3	rnsnop	$$⊢\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}=\left\{A\right\}$$
5	1	gidsn	$$⊢\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)=A$$
6	5	sneqi	$$⊢\left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}=\left\{A\right\}$$
7	4 6	difeq12i	$$⊢\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}=\left\{A\right\}\setminus \left\{A\right\}$$
8		difid	$$⊢\left\{A\right\}\setminus \left\{A\right\}=\varnothing$$
9	7 8	eqtri	$$⊢\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}=\varnothing$$
10	9	xpeq2i	$$⊢\left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\times \left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)=\left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\times \varnothing$$
11		xp0	$$⊢\left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\times \varnothing =\varnothing$$
12	10 11	eqtri	$$⊢\left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\times \left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)=\varnothing$$
13	12	reseq2i	$$⊢{\left\{⟨⟨A,A⟩,A⟩\right\}\upharpoonright }_{\left(\left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\times \left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\right)}={\left\{⟨⟨A,A⟩,A⟩\right\}\upharpoonright }_{\varnothing }$$
14		res0	$$⊢{\left\{⟨⟨A,A⟩,A⟩\right\}\upharpoonright }_{\varnothing }=\varnothing$$
15	13 14	eqtri	$$⊢{\left\{⟨⟨A,A⟩,A⟩\right\}\upharpoonright }_{\left(\left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\times \left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\right)}=\varnothing$$
16		snex	$$⊢\left\{⟨⟨A,A⟩,A⟩\right\}\in \mathrm{V}$$
17		isdivrngo	$$⊢\left\{⟨⟨A,A⟩,A⟩\right\}\in \mathrm{V}\to \left(⟨\left\{⟨⟨A,A⟩,A⟩\right\},\left\{⟨⟨A,A⟩,A⟩\right\}⟩\in \mathrm{DivRingOps}\leftrightarrow \left(⟨\left\{⟨⟨A,A⟩,A⟩\right\},\left\{⟨⟨A,A⟩,A⟩\right\}⟩\in \mathrm{RingOps}\wedge {\left\{⟨⟨A,A⟩,A⟩\right\}\upharpoonright }_{\left(\left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\times \left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\right)}\in \mathrm{GrpOp}\right)\right)$$
18	16 17	ax-mp	$$⊢⟨\left\{⟨⟨A,A⟩,A⟩\right\},\left\{⟨⟨A,A⟩,A⟩\right\}⟩\in \mathrm{DivRingOps}\leftrightarrow \left(⟨\left\{⟨⟨A,A⟩,A⟩\right\},\left\{⟨⟨A,A⟩,A⟩\right\}⟩\in \mathrm{RingOps}\wedge {\left\{⟨⟨A,A⟩,A⟩\right\}\upharpoonright }_{\left(\left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\times \left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\right)}\in \mathrm{GrpOp}\right)$$
19	18	simprbi	$$⊢⟨\left\{⟨⟨A,A⟩,A⟩\right\},\left\{⟨⟨A,A⟩,A⟩\right\}⟩\in \mathrm{DivRingOps}\to {\left\{⟨⟨A,A⟩,A⟩\right\}\upharpoonright }_{\left(\left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\times \left(\mathrm{ran}\left\{⟨⟨A,A⟩,A⟩\right\}\setminus \left\{\mathrm{GId}\left(\left\{⟨⟨A,A⟩,A⟩\right\}\right)\right\}\right)\right)}\in \mathrm{GrpOp}$$
20	15 19	eqeltrrid	$$⊢⟨\left\{⟨⟨A,A⟩,A⟩\right\},\left\{⟨⟨A,A⟩,A⟩\right\}⟩\in \mathrm{DivRingOps}\to \varnothing \in \mathrm{GrpOp}$$
21	2 20	mto	$$⊢\neg ⟨\left\{⟨⟨A,A⟩,A⟩\right\},\left\{⟨⟨A,A⟩,A⟩\right\}⟩\in \mathrm{DivRingOps}$$