Proof of Theorem zrdivrng
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 0ngrp 30530 | . 2
⊢  ¬
∅ ∈ GrpOp | 
| 2 |  | opex 5469 | . . . . . . . . . 10
⊢
〈𝐴, 𝐴〉 ∈ V | 
| 3 | 2 | rnsnop 6244 | . . . . . . . . 9
⊢ ran
{〈〈𝐴, 𝐴〉, 𝐴〉} = {𝐴} | 
| 4 |  | zrdivrng.1 | . . . . . . . . . . 11
⊢ 𝐴 ∈ V | 
| 5 | 4 | gidsn 37959 | . . . . . . . . . 10
⊢
(GId‘{〈〈𝐴, 𝐴〉, 𝐴〉}) = 𝐴 | 
| 6 | 5 | sneqi 4637 | . . . . . . . . 9
⊢
{(GId‘{〈〈𝐴, 𝐴〉, 𝐴〉})} = {𝐴} | 
| 7 | 3, 6 | difeq12i 4124 | . . . . . . . 8
⊢ (ran
{〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) = ({𝐴} ∖ {𝐴}) | 
| 8 |  | difid 4376 | . . . . . . . 8
⊢ ({𝐴} ∖ {𝐴}) = ∅ | 
| 9 | 7, 8 | eqtri 2765 | . . . . . . 7
⊢ (ran
{〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) = ∅ | 
| 10 | 9 | xpeq2i 5712 | . . . . . 6
⊢ ((ran
{〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × (ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})})) = ((ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × ∅) | 
| 11 |  | xp0 6178 | . . . . . 6
⊢ ((ran
{〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × ∅) =
∅ | 
| 12 | 10, 11 | eqtri 2765 | . . . . 5
⊢ ((ran
{〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × (ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})})) = ∅ | 
| 13 | 12 | reseq2i 5994 | . . . 4
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉} ↾ ((ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × (ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}))) = ({〈〈𝐴, 𝐴〉, 𝐴〉} ↾ ∅) | 
| 14 |  | res0 6001 | . . . 4
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉} ↾ ∅) =
∅ | 
| 15 | 13, 14 | eqtri 2765 | . . 3
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉} ↾ ((ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × (ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}))) = ∅ | 
| 16 |  | snex 5436 | . . . . 5
⊢
{〈〈𝐴,
𝐴〉, 𝐴〉} ∈ V | 
| 17 |  | isdivrngo 37957 | . . . . 5
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉} ∈ V →
(〈{〈〈𝐴,
𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉 ∈ DivRingOps ↔
(〈{〈〈𝐴,
𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉 ∈ RingOps ∧
({〈〈𝐴, 𝐴〉, 𝐴〉} ↾ ((ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × (ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}))) ∈
GrpOp))) | 
| 18 | 16, 17 | ax-mp 5 | . . . 4
⊢
(〈{〈〈𝐴, 𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉 ∈ DivRingOps ↔
(〈{〈〈𝐴,
𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉 ∈ RingOps ∧
({〈〈𝐴, 𝐴〉, 𝐴〉} ↾ ((ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × (ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}))) ∈ GrpOp)) | 
| 19 | 18 | simprbi 496 | . . 3
⊢
(〈{〈〈𝐴, 𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉 ∈ DivRingOps →
({〈〈𝐴, 𝐴〉, 𝐴〉} ↾ ((ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × (ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}))) ∈ GrpOp) | 
| 20 | 15, 19 | eqeltrrid 2846 | . 2
⊢
(〈{〈〈𝐴, 𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉 ∈ DivRingOps →
∅ ∈ GrpOp) | 
| 21 | 1, 20 | mto 197 | 1
⊢  ¬
〈{〈〈𝐴, 𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉 ∈
DivRingOps |