issubrg

Description: The subring predicate. (Contributed by Stefan O'Rear, 27-Nov-2014) (Proof shortened by AV, 12-Oct-2020)

	Ref	Expression
Hypotheses	issubrg.b	$⊢ B = {Base}_{R}$
	issubrg.i	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	issubrg	$⊢ A \in SubRing (R) \leftrightarrow ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq B \land \underset{˙}{1} \in A))$

Proof

Step	Hyp	Ref	Expression
1		issubrg.b	$⊢ B = {Base}_{R}$
2		issubrg.i	$⊢ \underset{˙}{1} = 1_{R}$
3		df-subrg	$⊢ SubRing = (r \in Ring ⟼ \{s \in 𝒫 {Base}_{r} \| (r ↾_{𝑠} s \in Ring \land 1_{r} \in s)\})$
4	3	mptrcl	$⊢ A \in SubRing (R) \to R \in Ring$
5		simpll	$⊢ ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq B \land \underset{˙}{1} \in A)) \to R \in Ring$
6		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
7	6 1	eqtr4di	$⊢ r = R \to {Base}_{r} = B$
8	7	pweqd	$⊢ r = R \to 𝒫 {Base}_{r} = 𝒫 B$
9		oveq1	$⊢ r = R \to r ↾_{𝑠} s = R ↾_{𝑠} s$
10	9	eleq1d	$⊢ r = R \to (r ↾_{𝑠} s \in Ring \leftrightarrow R ↾_{𝑠} s \in Ring)$
11		fveq2	$⊢ r = R \to 1_{r} = 1_{R}$
12	11 2	eqtr4di	$⊢ r = R \to 1_{r} = \underset{˙}{1}$
13	12	eleq1d	$⊢ r = R \to (1_{r} \in s \leftrightarrow \underset{˙}{1} \in s)$
14	10 13	anbi12d	$⊢ r = R \to ((r ↾_{𝑠} s \in Ring \land 1_{r} \in s) \leftrightarrow (R ↾_{𝑠} s \in Ring \land \underset{˙}{1} \in s))$
15	8 14	rabeqbidv	$⊢ r = R \to \{s \in 𝒫 {Base}_{r} \| (r ↾_{𝑠} s \in Ring \land 1_{r} \in s)\} = \{s \in 𝒫 B \| (R ↾_{𝑠} s \in Ring \land \underset{˙}{1} \in s)\}$
16	1	fvexi	$⊢ B \in V$
17	16	pwex	$⊢ 𝒫 B \in V$
18	17	rabex	$⊢ \{s \in 𝒫 B \| (R ↾_{𝑠} s \in Ring \land \underset{˙}{1} \in s)\} \in V$
19	15 3 18	fvmpt	$⊢ R \in Ring \to SubRing (R) = \{s \in 𝒫 B \| (R ↾_{𝑠} s \in Ring \land \underset{˙}{1} \in s)\}$
20	19	eleq2d	$⊢ R \in Ring \to (A \in SubRing (R) \leftrightarrow A \in \{s \in 𝒫 B \| (R ↾_{𝑠} s \in Ring \land \underset{˙}{1} \in s)\})$
21		oveq2	$⊢ s = A \to R ↾_{𝑠} s = R ↾_{𝑠} A$
22	21	eleq1d	$⊢ s = A \to (R ↾_{𝑠} s \in Ring \leftrightarrow R ↾_{𝑠} A \in Ring)$
23		eleq2	$⊢ s = A \to (\underset{˙}{1} \in s \leftrightarrow \underset{˙}{1} \in A)$
24	22 23	anbi12d	$⊢ s = A \to ((R ↾_{𝑠} s \in Ring \land \underset{˙}{1} \in s) \leftrightarrow (R ↾_{𝑠} A \in Ring \land \underset{˙}{1} \in A))$
25	24	elrab	$⊢ A \in \{s \in 𝒫 B \| (R ↾_{𝑠} s \in Ring \land \underset{˙}{1} \in s)\} \leftrightarrow (A \in 𝒫 B \land (R ↾_{𝑠} A \in Ring \land \underset{˙}{1} \in A))$
26	16	elpw2	$⊢ A \in 𝒫 B \leftrightarrow A \subseteq B$
27	26	anbi1i	$⊢ (A \in 𝒫 B \land (R ↾_{𝑠} A \in Ring \land \underset{˙}{1} \in A)) \leftrightarrow (A \subseteq B \land (R ↾_{𝑠} A \in Ring \land \underset{˙}{1} \in A))$
28		an12	$⊢ (A \subseteq B \land (R ↾_{𝑠} A \in Ring \land \underset{˙}{1} \in A)) \leftrightarrow (R ↾_{𝑠} A \in Ring \land (A \subseteq B \land \underset{˙}{1} \in A))$
29	25 27 28	3bitri	$⊢ A \in \{s \in 𝒫 B \| (R ↾_{𝑠} s \in Ring \land \underset{˙}{1} \in s)\} \leftrightarrow (R ↾_{𝑠} A \in Ring \land (A \subseteq B \land \underset{˙}{1} \in A))$
30		ibar	$⊢ R \in Ring \to (R ↾_{𝑠} A \in Ring \leftrightarrow (R \in Ring \land R ↾_{𝑠} A \in Ring))$
31	30	anbi1d	$⊢ R \in Ring \to ((R ↾_{𝑠} A \in Ring \land (A \subseteq B \land \underset{˙}{1} \in A)) \leftrightarrow ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq B \land \underset{˙}{1} \in A)))$
32	29 31	bitrid	$⊢ R \in Ring \to (A \in \{s \in 𝒫 B \| (R ↾_{𝑠} s \in Ring \land \underset{˙}{1} \in s)\} \leftrightarrow ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq B \land \underset{˙}{1} \in A)))$
33	20 32	bitrd	$⊢ R \in Ring \to (A \in SubRing (R) \leftrightarrow ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq B \land \underset{˙}{1} \in A)))$
34	4 5 33	pm5.21nii	$⊢ A \in SubRing (R) \leftrightarrow ((R \in Ring \land R ↾_{𝑠} A \in Ring) \land (A \subseteq B \land \underset{˙}{1} \in A))$

Metamath Proof Explorer

Theorem issubrg

Proof