| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | eqid 2737 | . . . . . 6
⊢
(oppr‘𝑄) = (oppr‘𝑄) | 
| 2 |  | eqid 2737 | . . . . . 6
⊢
(1r‘𝑄) = (1r‘𝑄) | 
| 3 | 1, 2 | oppr1 20350 | . . . . 5
⊢
(1r‘𝑄) =
(1r‘(oppr‘𝑄)) | 
| 4 |  | opprqus.b | . . . . . 6
⊢ 𝐵 = (Base‘𝑅) | 
| 5 |  | opprqus.o | . . . . . 6
⊢ 𝑂 =
(oppr‘𝑅) | 
| 6 |  | opprqus.q | . . . . . 6
⊢ 𝑄 = (𝑅 /s (𝑅 ~QG 𝐼)) | 
| 7 |  | opprqus1r.r | . . . . . 6
⊢ (𝜑 → 𝑅 ∈ Ring) | 
| 8 |  | opprqus1r.i | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑅)) | 
| 9 | 4, 5, 6, 7, 8 | opprqus1r 33520 | . . . . 5
⊢ (𝜑 →
(1r‘(oppr‘𝑄)) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼)))) | 
| 10 | 3, 9 | eqtrid 2789 | . . . 4
⊢ (𝜑 → (1r‘𝑄) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼)))) | 
| 11 |  | eqid 2737 | . . . . . 6
⊢
(0g‘𝑄) = (0g‘𝑄) | 
| 12 | 1, 11 | oppr0 20349 | . . . . 5
⊢
(0g‘𝑄) =
(0g‘(oppr‘𝑄)) | 
| 13 | 8 | 2idllidld 21264 | . . . . . . 7
⊢ (𝜑 → 𝐼 ∈ (LIdeal‘𝑅)) | 
| 14 |  | lidlnsg 21258 | . . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (LIdeal‘𝑅)) → 𝐼 ∈ (NrmSGrp‘𝑅)) | 
| 15 | 7, 13, 14 | syl2anc 584 | . . . . . 6
⊢ (𝜑 → 𝐼 ∈ (NrmSGrp‘𝑅)) | 
| 16 | 4, 5, 6, 15 | opprqus0g 33518 | . . . . 5
⊢ (𝜑 →
(0g‘(oppr‘𝑄)) = (0g‘(𝑂 /s (𝑂 ~QG 𝐼)))) | 
| 17 | 12, 16 | eqtrid 2789 | . . . 4
⊢ (𝜑 → (0g‘𝑄) = (0g‘(𝑂 /s (𝑂 ~QG 𝐼)))) | 
| 18 | 10, 17 | neeq12d 3002 | . . 3
⊢ (𝜑 →
((1r‘𝑄)
≠ (0g‘𝑄) ↔ (1r‘(𝑂 /s (𝑂 ~QG 𝐼))) ≠
(0g‘(𝑂
/s (𝑂
~QG 𝐼))))) | 
| 19 |  | eqid 2737 | . . . . . . 7
⊢
(Base‘𝑄) =
(Base‘𝑄) | 
| 20 | 1, 19 | opprbas 20341 | . . . . . 6
⊢
(Base‘𝑄) =
(Base‘(oppr‘𝑄)) | 
| 21 |  | eqid 2737 | . . . . . . . . 9
⊢
(LIdeal‘𝑅) =
(LIdeal‘𝑅) | 
| 22 | 4, 21 | lidlss 21222 | . . . . . . . 8
⊢ (𝐼 ∈ (LIdeal‘𝑅) → 𝐼 ⊆ 𝐵) | 
| 23 | 13, 22 | syl 17 | . . . . . . 7
⊢ (𝜑 → 𝐼 ⊆ 𝐵) | 
| 24 | 4, 5, 6, 7, 23 | opprqusbas 33516 | . . . . . 6
⊢ (𝜑 →
(Base‘(oppr‘𝑄)) = (Base‘(𝑂 /s (𝑂 ~QG 𝐼)))) | 
| 25 | 20, 24 | eqtrid 2789 | . . . . 5
⊢ (𝜑 → (Base‘𝑄) = (Base‘(𝑂 /s (𝑂 ~QG 𝐼)))) | 
| 26 | 17 | sneqd 4638 | . . . . 5
⊢ (𝜑 →
{(0g‘𝑄)} =
{(0g‘(𝑂
/s (𝑂
~QG 𝐼)))}) | 
| 27 | 25, 26 | difeq12d 4127 | . . . 4
⊢ (𝜑 → ((Base‘𝑄) ∖
{(0g‘𝑄)})
= ((Base‘(𝑂
/s (𝑂
~QG 𝐼)))
∖ {(0g‘(𝑂 /s (𝑂 ~QG 𝐼)))})) | 
| 28 | 25 | adantr 480 | . . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) → (Base‘𝑄) = (Base‘(𝑂 /s (𝑂 ~QG 𝐼)))) | 
| 29 | 7 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑦 ∈ (Base‘𝑄)) → 𝑅 ∈ Ring) | 
| 30 | 8 | ad2antrr 726 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑦 ∈ (Base‘𝑄)) → 𝐼 ∈ (2Ideal‘𝑅)) | 
| 31 |  | simplr 769 | . . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑦 ∈ (Base‘𝑄)) → 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) | 
| 32 | 31 | eldifad 3963 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑦 ∈ (Base‘𝑄)) → 𝑥 ∈ (Base‘𝑄)) | 
| 33 |  | simpr 484 | . . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑦 ∈ (Base‘𝑄)) → 𝑦 ∈ (Base‘𝑄)) | 
| 34 | 4, 5, 6, 29, 30, 19, 32, 33 | opprqusmulr 33519 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑦 ∈ (Base‘𝑄)) → (𝑥(.r‘(oppr‘𝑄))𝑦) = (𝑥(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑦)) | 
| 35 | 10 | ad2antrr 726 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑦 ∈ (Base‘𝑄)) → (1r‘𝑄) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼)))) | 
| 36 | 34, 35 | eqeq12d 2753 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑦 ∈ (Base‘𝑄)) → ((𝑥(.r‘(oppr‘𝑄))𝑦) = (1r‘𝑄) ↔ (𝑥(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑦) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼))))) | 
| 37 | 4, 5, 6, 29, 30, 19, 33, 32 | opprqusmulr 33519 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑦 ∈ (Base‘𝑄)) → (𝑦(.r‘(oppr‘𝑄))𝑥) = (𝑦(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑥)) | 
| 38 | 37, 35 | eqeq12d 2753 | . . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑦 ∈ (Base‘𝑄)) → ((𝑦(.r‘(oppr‘𝑄))𝑥) = (1r‘𝑄) ↔ (𝑦(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑥) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼))))) | 
| 39 | 36, 38 | anbi12d 632 | . . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) ∧ 𝑦 ∈ (Base‘𝑄)) → (((𝑥(.r‘(oppr‘𝑄))𝑦) = (1r‘𝑄) ∧ (𝑦(.r‘(oppr‘𝑄))𝑥) = (1r‘𝑄)) ↔ ((𝑥(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑦) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼))) ∧ (𝑦(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑥) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼)))))) | 
| 40 | 28, 39 | rexeqbidva 3333 | . . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})) → (∃𝑦 ∈ (Base‘𝑄)((𝑥(.r‘(oppr‘𝑄))𝑦) = (1r‘𝑄) ∧ (𝑦(.r‘(oppr‘𝑄))𝑥) = (1r‘𝑄)) ↔ ∃𝑦 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝐼)))((𝑥(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑦) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼))) ∧ (𝑦(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑥) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼)))))) | 
| 41 | 27, 40 | raleqbidva 3332 | . . 3
⊢ (𝜑 → (∀𝑥 ∈ ((Base‘𝑄) ∖
{(0g‘𝑄)})∃𝑦 ∈ (Base‘𝑄)((𝑥(.r‘(oppr‘𝑄))𝑦) = (1r‘𝑄) ∧ (𝑦(.r‘(oppr‘𝑄))𝑥) = (1r‘𝑄)) ↔ ∀𝑥 ∈ ((Base‘(𝑂 /s (𝑂 ~QG 𝐼))) ∖ {(0g‘(𝑂 /s (𝑂 ~QG 𝐼)))})∃𝑦 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝐼)))((𝑥(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑦) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼))) ∧ (𝑦(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑥) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼)))))) | 
| 42 | 18, 41 | anbi12d 632 | . 2
⊢ (𝜑 →
(((1r‘𝑄)
≠ (0g‘𝑄) ∧ ∀𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})∃𝑦 ∈ (Base‘𝑄)((𝑥(.r‘(oppr‘𝑄))𝑦) = (1r‘𝑄) ∧ (𝑦(.r‘(oppr‘𝑄))𝑥) = (1r‘𝑄))) ↔ ((1r‘(𝑂 /s (𝑂 ~QG 𝐼))) ≠ (0g‘(𝑂 /s (𝑂 ~QG 𝐼))) ∧ ∀𝑥 ∈ ((Base‘(𝑂 /s (𝑂 ~QG 𝐼))) ∖ {(0g‘(𝑂 /s (𝑂 ~QG 𝐼)))})∃𝑦 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝐼)))((𝑥(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑦) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼))) ∧ (𝑦(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑥) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼))))))) | 
| 43 |  | eqid 2737 | . . 3
⊢
(.r‘(oppr‘𝑄)) =
(.r‘(oppr‘𝑄)) | 
| 44 |  | eqid 2737 | . . . 4
⊢
(Unit‘𝑄) =
(Unit‘𝑄) | 
| 45 | 44, 1 | opprunit 20377 | . . 3
⊢
(Unit‘𝑄) =
(Unit‘(oppr‘𝑄)) | 
| 46 |  | eqid 2737 | . . . . . 6
⊢
(2Ideal‘𝑅) =
(2Ideal‘𝑅) | 
| 47 | 6, 46 | qusring 21285 | . . . . 5
⊢ ((𝑅 ∈ Ring ∧ 𝐼 ∈ (2Ideal‘𝑅)) → 𝑄 ∈ Ring) | 
| 48 | 7, 8, 47 | syl2anc 584 | . . . 4
⊢ (𝜑 → 𝑄 ∈ Ring) | 
| 49 | 1 | opprring 20347 | . . . 4
⊢ (𝑄 ∈ Ring →
(oppr‘𝑄) ∈ Ring) | 
| 50 | 48, 49 | syl 17 | . . 3
⊢ (𝜑 →
(oppr‘𝑄) ∈ Ring) | 
| 51 | 20, 12, 3, 43, 45, 50 | isdrng4 33298 | . 2
⊢ (𝜑 →
((oppr‘𝑄) ∈ DivRing ↔
((1r‘𝑄)
≠ (0g‘𝑄) ∧ ∀𝑥 ∈ ((Base‘𝑄) ∖ {(0g‘𝑄)})∃𝑦 ∈ (Base‘𝑄)((𝑥(.r‘(oppr‘𝑄))𝑦) = (1r‘𝑄) ∧ (𝑦(.r‘(oppr‘𝑄))𝑥) = (1r‘𝑄))))) | 
| 52 |  | eqid 2737 | . . 3
⊢
(Base‘(𝑂
/s (𝑂
~QG 𝐼)))
= (Base‘(𝑂
/s (𝑂
~QG 𝐼))) | 
| 53 |  | eqid 2737 | . . 3
⊢
(0g‘(𝑂 /s (𝑂 ~QG 𝐼))) = (0g‘(𝑂 /s (𝑂 ~QG 𝐼))) | 
| 54 |  | eqid 2737 | . . 3
⊢
(1r‘(𝑂 /s (𝑂 ~QG 𝐼))) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼))) | 
| 55 |  | eqid 2737 | . . 3
⊢
(.r‘(𝑂 /s (𝑂 ~QG 𝐼))) = (.r‘(𝑂 /s (𝑂 ~QG 𝐼))) | 
| 56 |  | eqid 2737 | . . 3
⊢
(Unit‘(𝑂
/s (𝑂
~QG 𝐼)))
= (Unit‘(𝑂
/s (𝑂
~QG 𝐼))) | 
| 57 | 5 | opprring 20347 | . . . . 5
⊢ (𝑅 ∈ Ring → 𝑂 ∈ Ring) | 
| 58 | 7, 57 | syl 17 | . . . 4
⊢ (𝜑 → 𝑂 ∈ Ring) | 
| 59 | 5, 7 | oppr2idl 33514 | . . . . 5
⊢ (𝜑 → (2Ideal‘𝑅) = (2Ideal‘𝑂)) | 
| 60 | 8, 59 | eleqtrd 2843 | . . . 4
⊢ (𝜑 → 𝐼 ∈ (2Ideal‘𝑂)) | 
| 61 |  | eqid 2737 | . . . . 5
⊢ (𝑂 /s (𝑂 ~QG 𝐼)) = (𝑂 /s (𝑂 ~QG 𝐼)) | 
| 62 |  | eqid 2737 | . . . . 5
⊢
(2Ideal‘𝑂) =
(2Ideal‘𝑂) | 
| 63 | 61, 62 | qusring 21285 | . . . 4
⊢ ((𝑂 ∈ Ring ∧ 𝐼 ∈ (2Ideal‘𝑂)) → (𝑂 /s (𝑂 ~QG 𝐼)) ∈ Ring) | 
| 64 | 58, 60, 63 | syl2anc 584 | . . 3
⊢ (𝜑 → (𝑂 /s (𝑂 ~QG 𝐼)) ∈ Ring) | 
| 65 | 52, 53, 54, 55, 56, 64 | isdrng4 33298 | . 2
⊢ (𝜑 → ((𝑂 /s (𝑂 ~QG 𝐼)) ∈ DivRing ↔
((1r‘(𝑂
/s (𝑂
~QG 𝐼)))
≠ (0g‘(𝑂 /s (𝑂 ~QG 𝐼))) ∧ ∀𝑥 ∈ ((Base‘(𝑂 /s (𝑂 ~QG 𝐼))) ∖ {(0g‘(𝑂 /s (𝑂 ~QG 𝐼)))})∃𝑦 ∈ (Base‘(𝑂 /s (𝑂 ~QG 𝐼)))((𝑥(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑦) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼))) ∧ (𝑦(.r‘(𝑂 /s (𝑂 ~QG 𝐼)))𝑥) = (1r‘(𝑂 /s (𝑂 ~QG 𝐼))))))) | 
| 66 | 42, 51, 65 | 3bitr4d 311 | 1
⊢ (𝜑 →
((oppr‘𝑄) ∈ DivRing ↔ (𝑂 /s (𝑂 ~QG 𝐼)) ∈ DivRing)) |