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 } ) ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )