Step | Hyp | Ref
| Expression |
1 | | 0ngrp 29502 |
. 2
⊢ ¬
∅ ∈ GrpOp |
2 | | opex 5425 |
. . . . . . . . . 10
⊢
⟨𝐴, 𝐴⟩ ∈ V |
3 | 2 | rnsnop 6180 |
. . . . . . . . 9
⊢ ran
{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} = {𝐴} |
4 | | zrdivrng.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ V |
5 | 4 | gidsn 36461 |
. . . . . . . . . 10
⊢
(GId‘{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}) = 𝐴 |
6 | 5 | sneqi 4601 |
. . . . . . . . 9
⊢
{(GId‘{⟨⟨𝐴, 𝐴⟩, 𝐴⟩})} = {𝐴} |
7 | 3, 6 | difeq12i 4084 |
. . . . . . . 8
⊢ (ran
{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})}) = ({𝐴} ∖ {𝐴}) |
8 | | difid 4334 |
. . . . . . . 8
⊢ ({𝐴} ∖ {𝐴}) = ∅ |
9 | 7, 8 | eqtri 2761 |
. . . . . . 7
⊢ (ran
{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})}) = ∅ |
10 | 9 | xpeq2i 5664 |
. . . . . 6
⊢ ((ran
{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})}) × (ran {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})})) = ((ran {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})}) × ∅) |
11 | | xp0 6114 |
. . . . . 6
⊢ ((ran
{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})}) × ∅) =
∅ |
12 | 10, 11 | eqtri 2761 |
. . . . 5
⊢ ((ran
{⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})}) × (ran {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})})) = ∅ |
13 | 12 | reseq2i 5938 |
. . . 4
⊢
({⟨⟨𝐴,
𝐴⟩, 𝐴⟩} ↾ ((ran {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})}) × (ran {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})}))) = ({⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ↾ ∅) |
14 | | res0 5945 |
. . . 4
⊢
({⟨⟨𝐴,
𝐴⟩, 𝐴⟩} ↾ ∅) =
∅ |
15 | 13, 14 | eqtri 2761 |
. . 3
⊢
({⟨⟨𝐴,
𝐴⟩, 𝐴⟩} ↾ ((ran {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})}) × (ran {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})}))) = ∅ |
16 | | snex 5392 |
. . . . 5
⊢
{⟨⟨𝐴,
𝐴⟩, 𝐴⟩} ∈ V |
17 | | isdivrngo 36459 |
. . . . 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 498 |
. . 3
⊢
(⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩ ∈ DivRingOps →
({⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ↾ ((ran {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})}) × (ran {⟨⟨𝐴, 𝐴⟩, 𝐴⟩} ∖
{(GId‘{⟨⟨𝐴,
𝐴⟩, 𝐴⟩})}))) ∈ GrpOp) |
20 | 15, 19 | eqeltrrid 2839 |
. 2
⊢
(⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩ ∈ DivRingOps →
∅ ∈ GrpOp) |
21 | 1, 20 | mto 196 |
1
⊢ ¬
⟨{⟨⟨𝐴, 𝐴⟩, 𝐴⟩}, {⟨⟨𝐴, 𝐴⟩, 𝐴⟩}⟩ ∈
DivRingOps |