Proof of Theorem zrdivrng
Step | Hyp | Ref
| Expression |
1 | | 0ngrp 28290 |
. 2
⊢ ¬
∅ ∈ GrpOp |
2 | | opex 5358 |
. . . . . . . . . 10
⊢
〈𝐴, 𝐴〉 ∈ V |
3 | 2 | rnsnop 6083 |
. . . . . . . . 9
⊢ ran
{〈〈𝐴, 𝐴〉, 𝐴〉} = {𝐴} |
4 | | zrdivrng.1 |
. . . . . . . . . . 11
⊢ 𝐴 ∈ V |
5 | 4 | gidsn 35232 |
. . . . . . . . . 10
⊢
(GId‘{〈〈𝐴, 𝐴〉, 𝐴〉}) = 𝐴 |
6 | 5 | sneqi 4580 |
. . . . . . . . 9
⊢
{(GId‘{〈〈𝐴, 𝐴〉, 𝐴〉})} = {𝐴} |
7 | 3, 6 | difeq12i 4099 |
. . . . . . . 8
⊢ (ran
{〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) = ({𝐴} ∖ {𝐴}) |
8 | | difid 4332 |
. . . . . . . 8
⊢ ({𝐴} ∖ {𝐴}) = ∅ |
9 | 7, 8 | eqtri 2846 |
. . . . . . 7
⊢ (ran
{〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) = ∅ |
10 | 9 | xpeq2i 5584 |
. . . . . 6
⊢ ((ran
{〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × (ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})})) = ((ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × ∅) |
11 | | xp0 6017 |
. . . . . 6
⊢ ((ran
{〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × ∅) =
∅ |
12 | 10, 11 | eqtri 2846 |
. . . . 5
⊢ ((ran
{〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × (ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})})) = ∅ |
13 | 12 | reseq2i 5852 |
. . . 4
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉} ↾ ((ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × (ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}))) = ({〈〈𝐴, 𝐴〉, 𝐴〉} ↾ ∅) |
14 | | res0 5859 |
. . . 4
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉} ↾ ∅) =
∅ |
15 | 13, 14 | eqtri 2846 |
. . 3
⊢
({〈〈𝐴,
𝐴〉, 𝐴〉} ↾ ((ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × (ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}))) = ∅ |
16 | | snex 5334 |
. . . . 5
⊢
{〈〈𝐴,
𝐴〉, 𝐴〉} ∈ V |
17 | | isdivrngo 35230 |
. . . . 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 499 |
. . 3
⊢
(〈{〈〈𝐴, 𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉 ∈ DivRingOps →
({〈〈𝐴, 𝐴〉, 𝐴〉} ↾ ((ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}) × (ran {〈〈𝐴, 𝐴〉, 𝐴〉} ∖
{(GId‘{〈〈𝐴,
𝐴〉, 𝐴〉})}))) ∈ GrpOp) |
20 | 15, 19 | eqeltrrid 2920 |
. 2
⊢
(〈{〈〈𝐴, 𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉 ∈ DivRingOps →
∅ ∈ GrpOp) |
21 | 1, 20 | mto 199 |
1
⊢ ¬
〈{〈〈𝐴, 𝐴〉, 𝐴〉}, {〈〈𝐴, 𝐴〉, 𝐴〉}〉 ∈
DivRingOps |