issubrngd2

Description: Prove a subring by closure (definition version). (Contributed by Stefan O'Rear, 7-Dec-2014)

	Ref	Expression
Hypotheses	issubrngd.s	$⊢ φ \to S = I ↾_{𝑠} D$
	issubrngd.z	$⊢ φ \to \underset{˙}{0} = 0_{I}$
	issubrngd.p	$⊢ φ \to \underset{˙}{+} = +_{I}$
	issubrngd.ss	$⊢ φ \to D \subseteq {Base}_{I}$
	issubrngd.zcl	$⊢ φ \to \underset{˙}{0} \in D$
	issubrngd.acl	$⊢ (φ \land x \in D \land y \in D) \to x \underset{˙}{+} y \in D$
	issubrngd.ncl	$⊢ (φ \land x \in D) \to {inv}_{g} (I) (x) \in D$
	issubrngd.o	$⊢ φ \to \underset{˙}{1} = 1_{I}$
	issubrngd.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{I}$
	issubrngd.ocl	$⊢ φ \to \underset{˙}{1} \in D$
	issubrngd.tcl	$⊢ (φ \land x \in D \land y \in D) \to x \underset{˙}{\cdot} y \in D$
	issubrngd.g	$⊢ φ \to I \in Ring$
Assertion	issubrngd2	$⊢ φ \to D \in SubRing (I)$

Proof

Step	Hyp	Ref	Expression
1		issubrngd.s	$⊢ φ \to S = I ↾_{𝑠} D$
2		issubrngd.z	$⊢ φ \to \underset{˙}{0} = 0_{I}$
3		issubrngd.p	$⊢ φ \to \underset{˙}{+} = +_{I}$
4		issubrngd.ss	$⊢ φ \to D \subseteq {Base}_{I}$
5		issubrngd.zcl	$⊢ φ \to \underset{˙}{0} \in D$
6		issubrngd.acl	$⊢ (φ \land x \in D \land y \in D) \to x \underset{˙}{+} y \in D$
7		issubrngd.ncl	$⊢ (φ \land x \in D) \to {inv}_{g} (I) (x) \in D$
8		issubrngd.o	$⊢ φ \to \underset{˙}{1} = 1_{I}$
9		issubrngd.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{I}$
10		issubrngd.ocl	$⊢ φ \to \underset{˙}{1} \in D$
11		issubrngd.tcl	$⊢ (φ \land x \in D \land y \in D) \to x \underset{˙}{\cdot} y \in D$
12		issubrngd.g	$⊢ φ \to I \in Ring$
13		ringgrp	$⊢ I \in Ring \to I \in Grp$
14	12 13	syl	$⊢ φ \to I \in Grp$
15	1 2 3 4 5 6 7 14	issubgrpd2	$⊢ φ \to D \in SubGrp (I)$
16	8 10	eqeltrrd	$⊢ φ \to 1_{I} \in D$
17	9	oveqdr	$⊢ (φ \land (x \in D \land y \in D)) \to x \underset{˙}{\cdot} y = x \cdot_{I} y$
18	11	3expb	$⊢ (φ \land (x \in D \land y \in D)) \to x \underset{˙}{\cdot} y \in D$
19	17 18	eqeltrrd	$⊢ (φ \land (x \in D \land y \in D)) \to x \cdot_{I} y \in D$
20	19	ralrimivva	$⊢ φ \to \forall x \in D \forall y \in D x \cdot_{I} y \in D$
21		eqid	$⊢ {Base}_{I} = {Base}_{I}$
22		eqid	$⊢ 1_{I} = 1_{I}$
23		eqid	$⊢ \cdot_{I} = \cdot_{I}$
24	21 22 23	issubrg2	$⊢ I \in Ring \to (D \in SubRing (I) \leftrightarrow (D \in SubGrp (I) \land 1_{I} \in D \land \forall x \in D \forall y \in D x \cdot_{I} y \in D))$
25	12 24	syl	$⊢ φ \to (D \in SubRing (I) \leftrightarrow (D \in SubGrp (I) \land 1_{I} \in D \land \forall x \in D \forall y \in D x \cdot_{I} y \in D))$
26	15 16 20 25	mpbir3and	$⊢ φ \to D \in SubRing (I)$

Metamath Proof Explorer

Theorem issubrngd2

Proof