Metamath Proof Explorer

Theorem issdrg

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

		Ref	Expression
	Assertion	issdrg	$⊢ S \in SubDRing (R) \leftrightarrow (R \in DivRing \land S \in SubRing (R) \land R ↾_{𝑠} S \in DivRing)$

Proof

Step	Hyp	Ref	Expression
1		df-sdrg	$⊢ SubDRing = (w \in DivRing ⟼ \{s \in SubRing (w) \| w ↾_{𝑠} s \in DivRing\})$
2	1	mptrcl	$⊢ S \in SubDRing (R) \to R \in DivRing$
3		fveq2	$⊢ w = R \to SubRing (w) = SubRing (R)$
4		oveq1	$⊢ w = R \to w ↾_{𝑠} s = R ↾_{𝑠} s$
5	4	eleq1d	$⊢ w = R \to (w ↾_{𝑠} s \in DivRing \leftrightarrow R ↾_{𝑠} s \in DivRing)$
6	3 5	rabeqbidv	$⊢ w = R \to \{s \in SubRing (w) \| w ↾_{𝑠} s \in DivRing\} = \{s \in SubRing (R) \| R ↾_{𝑠} s \in DivRing\}$
7		fvex	$⊢ SubRing (R) \in V$
8	7	rabex	$⊢ \{s \in SubRing (R) \| R ↾_{𝑠} s \in DivRing\} \in V$
9	6 1 8	fvmpt	$⊢ R \in DivRing \to SubDRing (R) = \{s \in SubRing (R) \| R ↾_{𝑠} s \in DivRing\}$
10	9	eleq2d	$⊢ R \in DivRing \to (S \in SubDRing (R) \leftrightarrow S \in \{s \in SubRing (R) \| R ↾_{𝑠} s \in DivRing\})$
11		oveq2	$⊢ s = S \to R ↾_{𝑠} s = R ↾_{𝑠} S$
12	11	eleq1d	$⊢ s = S \to (R ↾_{𝑠} s \in DivRing \leftrightarrow R ↾_{𝑠} S \in DivRing)$
13	12	elrab	$⊢ S \in \{s \in SubRing (R) \| R ↾_{𝑠} s \in DivRing\} \leftrightarrow (S \in SubRing (R) \land R ↾_{𝑠} S \in DivRing)$
14	10 13	bitrdi	$⊢ R \in DivRing \to (S \in SubDRing (R) \leftrightarrow (S \in SubRing (R) \land R ↾_{𝑠} S \in DivRing))$
15	2 14	biadanii	$⊢ S \in SubDRing (R) \leftrightarrow (R \in DivRing \land (S \in SubRing (R) \land R ↾_{𝑠} S \in DivRing))$
16		3anass	$⊢ (R \in DivRing \land S \in SubRing (R) \land R ↾_{𝑠} S \in DivRing) \leftrightarrow (R \in DivRing \land (S \in SubRing (R) \land R ↾_{𝑠} S \in DivRing))$
17	15 16	bitr4i	$⊢ S \in SubDRing (R) \leftrightarrow (R \in DivRing \land S \in SubRing (R) \land R ↾_{𝑠} S \in DivRing)$