Metamath Proof Explorer


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