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

Metamath Proof Explorer

Theorem issdrg2

Description: Property of a division subring (closure version). (Contributed by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypotheses issdrg2.i ⊢ 𝐼 = ( invr ‘ 𝑅 )
issdrg2.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion issdrg2 ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( 𝑆 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 issdrg2.i ⊢ 𝐼 = ( invr ‘ 𝑅 )
2 issdrg2.z ⊢ 0 = ( 0g ‘ 𝑅 )
3 issdrg ⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) )
4 eqid ⊢ ( 𝑅 ↾s 𝑆 ) = ( 𝑅 ↾s 𝑆 )
5 4 2 1 issubdrg ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) → ( ( 𝑅 ↾s 𝑆 ) ∈ DivRing ↔ ∀ 𝑥 ∈ ( 𝑆 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )
6 5 pm5.32i ⊢ ( ( ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) ↔ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝑆 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )
7 df-3an ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) ↔ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) )
8 df-3an ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( 𝑆 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ↔ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ) ∧ ∀ 𝑥 ∈ ( 𝑆 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )
9 6 7 8 3bitr4i ⊢ ( ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ( 𝑅 ↾s 𝑆 ) ∈ DivRing ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( 𝑆 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )
10 3 9 bitri ⊢ ( 𝑆 ∈ ( SubDRing ‘ 𝑅 ) ↔ ( 𝑅 ∈ DivRing ∧ 𝑆 ∈ ( SubRing ‘ 𝑅 ) ∧ ∀ 𝑥 ∈ ( 𝑆 ∖ { 0 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )