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	⊢ 𝐴 ∈ V
Assertion	zrdivrng	⊢ ¬ ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ∈ DivRingOps

Proof

Step	Hyp	Ref	Expression
1		zrdivrng.1	⊢ 𝐴 ∈ V
2		0ngrp	⊢ ¬ ∅ ∈ GrpOp
3		opex	⊢ ⟨ 𝐴 , 𝐴 ⟩ ∈ V
4	3	rnsnop	⊢ ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } = { 𝐴 }
5	1	gidsn	⊢ ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) = 𝐴
6	5	sneqi	⊢ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } = { 𝐴 }
7	4 6	difeq12i	⊢ ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) = ( { 𝐴 } ∖ { 𝐴 } )
8		difid	⊢ ( { 𝐴 } ∖ { 𝐴 } ) = ∅
9	7 8	eqtri	⊢ ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) = ∅
10	9	xpeq2i	⊢ ( ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) × ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) ) = ( ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) × ∅ )
11		xp0	⊢ ( ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) × ∅ ) = ∅
12	10 11	eqtri	⊢ ( ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) × ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) ) = ∅
13	12	reseq2i	⊢ ( { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ↾ ( ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) × ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) ) ) = ( { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ↾ ∅ )
14		res0	⊢ ( { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ↾ ∅ ) = ∅
15	13 14	eqtri	⊢ ( { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ↾ ( ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) × ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) ) ) = ∅
16		snex	⊢ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∈ V
17		isdivrngo	⊢ ( { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∈ V → ( ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ∈ DivRingOps ↔ ( ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ∈ RingOps ∧ ( { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ↾ ( ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) × ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) ) ) ∈ GrpOp ) ) )
18	16 17	ax-mp	⊢ ( ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ∈ DivRingOps ↔ ( ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ∈ RingOps ∧ ( { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ↾ ( ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) × ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) ) ) ∈ GrpOp ) )
19	18	simprbi	⊢ ( ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ∈ DivRingOps → ( { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ↾ ( ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) × ( ran { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ∖ { ( GId ‘ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ) } ) ) ) ∈ GrpOp )
20	15 19	eqeltrrid	⊢ ( ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ∈ DivRingOps → ∅ ∈ GrpOp )
21	2 20	mto	⊢ ¬ ⟨ { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } , { ⟨ ⟨ 𝐴 , 𝐴 ⟩ , 𝐴 ⟩ } ⟩ ∈ DivRingOps