This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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