Metamath Proof Explorer

Theorem issdrg

Description: Property of a division subring. (Contributed by Stefan O'Rear, 3-Oct-2015)

Ref Expression
Assertion issdrg ⊢ S ∈ SubDRing ⁡ R ↔ R ∈ DivRing ∧ S ∈ SubRing ⁡ R ∧ R ↾ 𝑠 S ∈ DivRing

Proof

Step Hyp Ref Expression
1 df-sdrg ⊢ SubDRing = w ∈ DivRing ⟼ s ∈ SubRing ⁡ w | w ↾ 𝑠 s ∈ DivRing
2 1 mptrcl ⊢ S ∈ SubDRing ⁡ R → R ∈ DivRing
3 fveq2 ⊢ w = R → SubRing ⁡ w = SubRing ⁡ R
4 oveq1 ⊢ w = R → w ↾ 𝑠 s = R ↾ 𝑠 s
5 4 eleq1d ⊢ w = R → w ↾ 𝑠 s ∈ DivRing ↔ R ↾ 𝑠 s ∈ DivRing
6 3 5 rabeqbidv ⊢ w = R → s ∈ SubRing ⁡ w | w ↾ 𝑠 s ∈ DivRing = s ∈ SubRing ⁡ R | R ↾ 𝑠 s ∈ DivRing
7 fvex ⊢ SubRing ⁡ R ∈ V
8 7 rabex ⊢ s ∈ SubRing ⁡ R | R ↾ 𝑠 s ∈ DivRing ∈ V
9 6 1 8 fvmpt ⊢ R ∈ DivRing → SubDRing ⁡ R = s ∈ SubRing ⁡ R | R ↾ 𝑠 s ∈ DivRing
10 9 eleq2d ⊢ R ∈ DivRing → S ∈ SubDRing ⁡ R ↔ S ∈ s ∈ SubRing ⁡ R | R ↾ 𝑠 s ∈ DivRing
11 oveq2 ⊢ s = S → R ↾ 𝑠 s = R ↾ 𝑠 S
12 11 eleq1d ⊢ s = S → R ↾ 𝑠 s ∈ DivRing ↔ R ↾ 𝑠 S ∈ DivRing
13 12 elrab ⊢ S ∈ s ∈ SubRing ⁡ R | R ↾ 𝑠 s ∈ DivRing ↔ S ∈ SubRing ⁡ R ∧ R ↾ 𝑠 S ∈ DivRing
14 10 13 bitrdi ⊢ R ∈ DivRing → S ∈ SubDRing ⁡ R ↔ S ∈ SubRing ⁡ R ∧ R ↾ 𝑠 S ∈ DivRing
15 2 14 biadanii ⊢ S ∈ SubDRing ⁡ R ↔ R ∈ DivRing ∧ S ∈ SubRing ⁡ R ∧ R ↾ 𝑠 S ∈ DivRing
16 3anass ⊢ R ∈ DivRing ∧ S ∈ SubRing ⁡ R ∧ R ↾ 𝑠 S ∈ DivRing ↔ R ∈ DivRing ∧ S ∈ SubRing ⁡ R ∧ R ↾ 𝑠 S ∈ DivRing
17 15 16 bitr4i ⊢ S ∈ SubDRing ⁡ R ↔ R ∈ DivRing ∧ S ∈ SubRing ⁡ R ∧ R ↾ 𝑠 S ∈ DivRing