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 ) )