issubrng

Description: The subring of non-unital ring predicate. (Contributed by AV, 14-Feb-2025)

		Ref	Expression
	Hypothesis	issubrng.b	$⊢ B = {Base}_{R}$
	Assertion	issubrng	$⊢ A \in SubRng (R) \leftrightarrow (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B)$

Proof

Step	Hyp	Ref	Expression
1		issubrng.b	$⊢ B = {Base}_{R}$
2		df-subrng	$⊢ SubRng = (w \in Rng ⟼ \{s \in 𝒫 {Base}_{w} \| w ↾_{𝑠} s \in Rng\})$
3	2	mptrcl	$⊢ A \in SubRng (R) \to R \in Rng$
4		simp1	$⊢ (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B) \to R \in Rng$
5		fveq2	$⊢ r = R \to {Base}_{r} = {Base}_{R}$
6	5	pweqd	$⊢ r = R \to 𝒫 {Base}_{r} = 𝒫 {Base}_{R}$
7		oveq1	$⊢ r = R \to r ↾_{𝑠} s = R ↾_{𝑠} s$
8	7	eleq1d	$⊢ r = R \to (r ↾_{𝑠} s \in Rng \leftrightarrow R ↾_{𝑠} s \in Rng)$
9	6 8	rabeqbidv	$⊢ r = R \to \{s \in 𝒫 {Base}_{r} \| r ↾_{𝑠} s \in Rng\} = \{s \in 𝒫 {Base}_{R} \| R ↾_{𝑠} s \in Rng\}$
10		df-subrng	$⊢ SubRng = (r \in Rng ⟼ \{s \in 𝒫 {Base}_{r} \| r ↾_{𝑠} s \in Rng\})$
11		fvex	$⊢ {Base}_{R} \in V$
12	11	pwex	$⊢ 𝒫 {Base}_{R} \in V$
13	12	rabex	$⊢ \{s \in 𝒫 {Base}_{R} \| R ↾_{𝑠} s \in Rng\} \in V$
14	9 10 13	fvmpt	$⊢ R \in Rng \to SubRng (R) = \{s \in 𝒫 {Base}_{R} \| R ↾_{𝑠} s \in Rng\}$
15	14	eleq2d	$⊢ R \in Rng \to (A \in SubRng (R) \leftrightarrow A \in \{s \in 𝒫 {Base}_{R} \| R ↾_{𝑠} s \in Rng\})$
16		oveq2	$⊢ s = A \to R ↾_{𝑠} s = R ↾_{𝑠} A$
17	16	eleq1d	$⊢ s = A \to (R ↾_{𝑠} s \in Rng \leftrightarrow R ↾_{𝑠} A \in Rng)$
18	17	elrab	$⊢ A \in \{s \in 𝒫 {Base}_{R} \| R ↾_{𝑠} s \in Rng\} \leftrightarrow (A \in 𝒫 {Base}_{R} \land R ↾_{𝑠} A \in Rng)$
19	1	eqcomi	$⊢ {Base}_{R} = B$
20	19	sseq2i	$⊢ A \subseteq {Base}_{R} \leftrightarrow A \subseteq B$
21	20	anbi2i	$⊢ (R ↾_{𝑠} A \in Rng \land A \subseteq {Base}_{R}) \leftrightarrow (R ↾_{𝑠} A \in Rng \land A \subseteq B)$
22		ibar	$⊢ R \in Rng \to ((R ↾_{𝑠} A \in Rng \land A \subseteq B) \leftrightarrow (R \in Rng \land (R ↾_{𝑠} A \in Rng \land A \subseteq B)))$
23	21 22	bitrid	$⊢ R \in Rng \to ((R ↾_{𝑠} A \in Rng \land A \subseteq {Base}_{R}) \leftrightarrow (R \in Rng \land (R ↾_{𝑠} A \in Rng \land A \subseteq B)))$
24	11	elpw2	$⊢ A \in 𝒫 {Base}_{R} \leftrightarrow A \subseteq {Base}_{R}$
25	24	anbi2ci	$⊢ (A \in 𝒫 {Base}_{R} \land R ↾_{𝑠} A \in Rng) \leftrightarrow (R ↾_{𝑠} A \in Rng \land A \subseteq {Base}_{R})$
26		3anass	$⊢ (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B) \leftrightarrow (R \in Rng \land (R ↾_{𝑠} A \in Rng \land A \subseteq B))$
27	23 25 26	3bitr4g	$⊢ R \in Rng \to ((A \in 𝒫 {Base}_{R} \land R ↾_{𝑠} A \in Rng) \leftrightarrow (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B))$
28	18 27	bitrid	$⊢ R \in Rng \to (A \in \{s \in 𝒫 {Base}_{R} \| R ↾_{𝑠} s \in Rng\} \leftrightarrow (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B))$
29	15 28	bitrd	$⊢ R \in Rng \to (A \in SubRng (R) \leftrightarrow (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B))$
30	3 4 29	pm5.21nii	$⊢ A \in SubRng (R) \leftrightarrow (R \in Rng \land R ↾_{𝑠} A \in Rng \land A \subseteq B)$

Metamath Proof Explorer

Theorem issubrng

Proof