issubrgd

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

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

Proof

Step	Hyp	Ref	Expression
1		issubrgd.s	$⊢ φ \to S = I ↾_{𝑠} D$
2		issubrgd.z	$⊢ φ \to \underset{˙}{0} = 0_{I}$
3		issubrgd.p	$⊢ φ \to \underset{˙}{+} = +_{I}$
4		issubrgd.ss	$⊢ φ \to D \subseteq {Base}_{I}$
5		issubrgd.zcl	$⊢ φ \to \underset{˙}{0} \in D$
6		issubrgd.acl	$⊢ (φ \land x \in D \land y \in D) \to x \underset{˙}{+} y \in D$
7		issubrgd.ncl	$⊢ (φ \land x \in D) \to {inv}_{g} (I) (x) \in D$
8		issubrgd.o	$⊢ φ \to \underset{˙}{1} = 1_{I}$
9		issubrgd.t	$⊢ φ \to \underset{˙}{\cdot} = \cdot_{I}$
10		issubrgd.ocl	$⊢ φ \to \underset{˙}{1} \in D$
11		issubrgd.tcl	$⊢ (φ \land x \in D \land y \in D) \to x \underset{˙}{\cdot} y \in D$
12		issubrgd.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 issubrgd

Proof