issdrg2

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

	Ref	Expression
Hypotheses	issdrg2.i	$⊢ I = {inv}_{r} (R)$
	issdrg2.z	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	issdrg2	$⊢ S \in SubDRing (R) \leftrightarrow (R \in DivRing \land S \in SubRing (R) \land \forall x \in (S ∖ \{\underset{˙}{0}\}) I (x) \in S)$

Step	Hyp	Ref	Expression
1		issdrg2.i	$⊢ I = {inv}_{r} (R)$
2		issdrg2.z	$⊢ \underset{˙}{0} = 0_{R}$
3		issdrg	$⊢ S \in SubDRing (R) \leftrightarrow (R \in DivRing \land S \in SubRing (R) \land R ↾_{𝑠} S \in DivRing)$
4		eqid	$⊢ R ↾_{𝑠} S = R ↾_{𝑠} S$
5	4 2 1	issubdrg	$⊢ (R \in DivRing \land S \in SubRing (R)) \to (R ↾_{𝑠} S \in DivRing \leftrightarrow \forall x \in (S ∖ \{\underset{˙}{0}\}) I (x) \in S)$
6	5	pm5.32i	$⊢ ((R \in DivRing \land S \in SubRing (R)) \land R ↾_{𝑠} S \in DivRing) \leftrightarrow ((R \in DivRing \land S \in SubRing (R)) \land \forall x \in (S ∖ \{\underset{˙}{0}\}) I (x) \in S)$
7		df-3an	$⊢ (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)$
8		df-3an	$⊢ (R \in DivRing \land S \in SubRing (R) \land \forall x \in (S ∖ \{\underset{˙}{0}\}) I (x) \in S) \leftrightarrow ((R \in DivRing \land S \in SubRing (R)) \land \forall x \in (S ∖ \{\underset{˙}{0}\}) I (x) \in S)$
9	6 7 8	3bitr4i	$⊢ (R \in DivRing \land S \in SubRing (R) \land R ↾_{𝑠} S \in DivRing) \leftrightarrow (R \in DivRing \land S \in SubRing (R) \land \forall x \in (S ∖ \{\underset{˙}{0}\}) I (x) \in S)$
10	3 9	bitri	$⊢ S \in SubDRing (R) \leftrightarrow (R \in DivRing \land S \in SubRing (R) \land \forall x \in (S ∖ \{\underset{˙}{0}\}) I (x) \in S)$

Metamath Proof Explorer