This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem issdrg

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

Ref Expression
Assertion issdrg ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) )

Proof

Step Hyp Ref Expression
1 df-sdrg ⊢ SubDRing = ( 𝑤 ∈ DivRing ↦ { 𝑠 ∈ ( SubRing ‘ 𝑤 ) ∣ ( 𝑤 ↾s 𝑠 ) ∈ DivRing } )
2 1 mptrcl ⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) → 𝑅 ∈ DivRing )
3 fveq2 ⊢ ( 𝑤 = 𝑅 → ( SubRing ‘ 𝑤 ) = ( SubRing ‘ 𝑅 ) )
4 oveq1 ⊢ ( 𝑤 = 𝑅 → ( 𝑤 ↾s 𝑠 ) = ( 𝑅 ↾s 𝑠 ) )
5 4 eleq1d ⊢ ( 𝑤 = 𝑅 → ( ( 𝑤 ↾s 𝑠 ) ∈ DivRing ↔ ( 𝑅 ↾s 𝑠 ) ∈ DivRing ) )
6 3 5 rabeqbidv ⊢ ( 𝑤 = 𝑅 → { 𝑠 ∈ ( SubRing ‘ 𝑤 ) ∣ ( 𝑤 ↾s 𝑠 ) ∈ DivRing } = { 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ DivRing } )
7 fvex ⊢ ( SubRing ‘ 𝑅 ) ∈ V
8 7 rabex ⊢ { 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ DivRing } ∈ V
9 6 1 8 fvmpt ⊢ ( 𝑅 ∈ DivRing → ( SubDRing ‘ 𝑅 ) = { 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ DivRing } )
10 9 eleq2d ⊢ ( 𝑅 ∈ DivRing → ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) ↔ 𝑆 ∈ { 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ DivRing } ) )
11 oveq2 ⊢ ( 𝑠 = 𝑆 → ( 𝑅 ↾s 𝑠 ) = ( 𝑅 ↾s 𝑆 ) )
12 11 eleq1d ⊢ ( 𝑠 = 𝑆 → ( ( 𝑅 ↾s 𝑠 ) ∈ DivRing ↔ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) )
13 12 elrab ⊢ ( 𝑆 ∈ { 𝑠 ∈ ( SubRing ‘ 𝑅 ) ∣ ( 𝑅 ↾s 𝑠 ) ∈ DivRing } ↔ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) )
14 10 13 bitrdi ⊢ ( 𝑅 ∈ DivRing → ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) ) )
15 2 14 biadanii ⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) ) )
16 3anass ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) ↔ ( 𝑅 ∈ DivRing ∧ ( 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) ) )
17 15 16 bitr4i ⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) )