rnglidlmcl

Description: A (left) ideal containing the zero element is closed under left-multiplication by elements of the full non-unital ring. If the ring is not a unital ring, and the ideal does not contain the zero element of the ring, then the closure cannot be proven as in lidlmcl . (Contributed by AV, 18-Feb-2025)

	Ref	Expression
Hypotheses	rnglidlmcl.z	$⊢ \underset{˙}{0} = 0_{R}$
	rnglidlmcl.b	$⊢ B = {Base}_{R}$
	rnglidlmcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	rnglidlmcl.u	$⊢ U = LIdeal (R)$
Assertion	rnglidlmcl	$⊢ ((R \in Rng \land I \in U \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to X \underset{˙}{\cdot} Y \in I$

Proof

Step	Hyp	Ref	Expression
1		rnglidlmcl.z	$⊢ \underset{˙}{0} = 0_{R}$
2		rnglidlmcl.b	$⊢ B = {Base}_{R}$
3		rnglidlmcl.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
4		rnglidlmcl.u	$⊢ U = LIdeal (R)$
5		eqid	$⊢ +_{R} = +_{R}$
6	4 2 5 3	islidl	$⊢ I \in U \leftrightarrow (I \subseteq B \land I \neq \emptyset \land \forall x \in B \forall a \in I \forall b \in I (x \underset{˙}{\cdot} a) +_{R} b \in I)$
7		oveq1	$⊢ x = X \to x \underset{˙}{\cdot} a = X \underset{˙}{\cdot} a$
8	7	oveq1d	$⊢ x = X \to (x \underset{˙}{\cdot} a) +_{R} b = (X \underset{˙}{\cdot} a) +_{R} b$
9	8	eleq1d	$⊢ x = X \to ((x \underset{˙}{\cdot} a) +_{R} b \in I \leftrightarrow (X \underset{˙}{\cdot} a) +_{R} b \in I)$
10	9	ralbidv	$⊢ x = X \to (\forall b \in I (x \underset{˙}{\cdot} a) +_{R} b \in I \leftrightarrow \forall b \in I (X \underset{˙}{\cdot} a) +_{R} b \in I)$
11		oveq2	$⊢ a = Y \to X \underset{˙}{\cdot} a = X \underset{˙}{\cdot} Y$
12	11	oveq1d	$⊢ a = Y \to (X \underset{˙}{\cdot} a) +_{R} b = (X \underset{˙}{\cdot} Y) +_{R} b$
13	12	eleq1d	$⊢ a = Y \to ((X \underset{˙}{\cdot} a) +_{R} b \in I \leftrightarrow (X \underset{˙}{\cdot} Y) +_{R} b \in I)$
14	13	ralbidv	$⊢ a = Y \to (\forall b \in I (X \underset{˙}{\cdot} a) +_{R} b \in I \leftrightarrow \forall b \in I (X \underset{˙}{\cdot} Y) +_{R} b \in I)$
15	10 14	rspc2v	$⊢ (X \in B \land Y \in I) \to (\forall x \in B \forall a \in I \forall b \in I (x \underset{˙}{\cdot} a) +_{R} b \in I \to \forall b \in I (X \underset{˙}{\cdot} Y) +_{R} b \in I)$
16	15	adantl	$⊢ (((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to (\forall x \in B \forall a \in I \forall b \in I (x \underset{˙}{\cdot} a) +_{R} b \in I \to \forall b \in I (X \underset{˙}{\cdot} Y) +_{R} b \in I)$
17		oveq2	$⊢ b = \underset{˙}{0} \to (X \underset{˙}{\cdot} Y) +_{R} b = (X \underset{˙}{\cdot} Y) +_{R} \underset{˙}{0}$
18	17	eleq1d	$⊢ b = \underset{˙}{0} \to ((X \underset{˙}{\cdot} Y) +_{R} b \in I \leftrightarrow (X \underset{˙}{\cdot} Y) +_{R} \underset{˙}{0} \in I)$
19	18	rspcv	$⊢ \underset{˙}{0} \in I \to (\forall b \in I (X \underset{˙}{\cdot} Y) +_{R} b \in I \to (X \underset{˙}{\cdot} Y) +_{R} \underset{˙}{0} \in I)$
20	19	adantl	$⊢ ((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \to (\forall b \in I (X \underset{˙}{\cdot} Y) +_{R} b \in I \to (X \underset{˙}{\cdot} Y) +_{R} \underset{˙}{0} \in I)$
21		rnggrp	$⊢ R \in Rng \to R \in Grp$
22	21	3ad2ant1	$⊢ (R \in Rng \land I \subseteq B \land I \neq \emptyset) \to R \in Grp$
23	22	adantr	$⊢ ((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \to R \in Grp$
24	23	adantr	$⊢ (((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to R \in Grp$
25		simpll1	$⊢ (((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to R \in Rng$
26		simprl	$⊢ (((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to X \in B$
27		ssel	$⊢ I \subseteq B \to (Y \in I \to Y \in B)$
28	27	3ad2ant2	$⊢ (R \in Rng \land I \subseteq B \land I \neq \emptyset) \to (Y \in I \to Y \in B)$
29	28	adantr	$⊢ ((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \to (Y \in I \to Y \in B)$
30	29	adantld	$⊢ ((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \to ((X \in B \land Y \in I) \to Y \in B)$
31	30	imp	$⊢ (((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to Y \in B$
32	2 3	rngcl	$⊢ (R \in Rng \land X \in B \land Y \in B) \to X \underset{˙}{\cdot} Y \in B$
33	25 26 31 32	syl3anc	$⊢ (((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to X \underset{˙}{\cdot} Y \in B$
34	2 5 1 24 33	grpridd	$⊢ (((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to (X \underset{˙}{\cdot} Y) +_{R} \underset{˙}{0} = X \underset{˙}{\cdot} Y$
35	34	eleq1d	$⊢ (((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to ((X \underset{˙}{\cdot} Y) +_{R} \underset{˙}{0} \in I \leftrightarrow X \underset{˙}{\cdot} Y \in I)$
36	35	biimpd	$⊢ (((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to ((X \underset{˙}{\cdot} Y) +_{R} \underset{˙}{0} \in I \to X \underset{˙}{\cdot} Y \in I)$
37	36	ex	$⊢ ((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \to ((X \in B \land Y \in I) \to ((X \underset{˙}{\cdot} Y) +_{R} \underset{˙}{0} \in I \to X \underset{˙}{\cdot} Y \in I))$
38	20 37	syl5d	$⊢ ((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \to ((X \in B \land Y \in I) \to (\forall b \in I (X \underset{˙}{\cdot} Y) +_{R} b \in I \to X \underset{˙}{\cdot} Y \in I))$
39	38	imp	$⊢ (((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to (\forall b \in I (X \underset{˙}{\cdot} Y) +_{R} b \in I \to X \underset{˙}{\cdot} Y \in I)$
40	16 39	syld	$⊢ (((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to (\forall x \in B \forall a \in I \forall b \in I (x \underset{˙}{\cdot} a) +_{R} b \in I \to X \underset{˙}{\cdot} Y \in I)$
41	40	ex	$⊢ ((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \to ((X \in B \land Y \in I) \to (\forall x \in B \forall a \in I \forall b \in I (x \underset{˙}{\cdot} a) +_{R} b \in I \to X \underset{˙}{\cdot} Y \in I))$
42	41	com23	$⊢ ((R \in Rng \land I \subseteq B \land I \neq \emptyset) \land \underset{˙}{0} \in I) \to (\forall x \in B \forall a \in I \forall b \in I (x \underset{˙}{\cdot} a) +_{R} b \in I \to ((X \in B \land Y \in I) \to X \underset{˙}{\cdot} Y \in I))$
43	42	ex	$⊢ (R \in Rng \land I \subseteq B \land I \neq \emptyset) \to (\underset{˙}{0} \in I \to (\forall x \in B \forall a \in I \forall b \in I (x \underset{˙}{\cdot} a) +_{R} b \in I \to ((X \in B \land Y \in I) \to X \underset{˙}{\cdot} Y \in I)))$
44	43	com23	$⊢ (R \in Rng \land I \subseteq B \land I \neq \emptyset) \to (\forall x \in B \forall a \in I \forall b \in I (x \underset{˙}{\cdot} a) +_{R} b \in I \to (\underset{˙}{0} \in I \to ((X \in B \land Y \in I) \to X \underset{˙}{\cdot} Y \in I)))$
45	44	3exp	$⊢ R \in Rng \to (I \subseteq B \to (I \neq \emptyset \to (\forall x \in B \forall a \in I \forall b \in I (x \underset{˙}{\cdot} a) +_{R} b \in I \to (\underset{˙}{0} \in I \to ((X \in B \land Y \in I) \to X \underset{˙}{\cdot} Y \in I)))))$
46	45	3impd	$⊢ R \in Rng \to ((I \subseteq B \land I \neq \emptyset \land \forall x \in B \forall a \in I \forall b \in I (x \underset{˙}{\cdot} a) +_{R} b \in I) \to (\underset{˙}{0} \in I \to ((X \in B \land Y \in I) \to X \underset{˙}{\cdot} Y \in I)))$
47	6 46	biimtrid	$⊢ R \in Rng \to (I \in U \to (\underset{˙}{0} \in I \to ((X \in B \land Y \in I) \to X \underset{˙}{\cdot} Y \in I)))$
48	47	3imp1	$⊢ ((R \in Rng \land I \in U \land \underset{˙}{0} \in I) \land (X \in B \land Y \in I)) \to X \underset{˙}{\cdot} Y \in I$

Metamath Proof Explorer

Theorem rnglidlmcl

Proof