rnglidlrng

Description: A (left) ideal of a non-unital ring is a non-unital ring. (Contributed by AV, 17-Feb-2020) Generalization for non-unital rings. The assumption U e. ( SubGrpR ) is required because a left ideal of a non-unital ring does not have to be a subgroup. (Revised by AV, 11-Mar-2025)

	Ref	Expression
Hypotheses	rnglidlabl.l	$⊢ L = LIdeal (R)$
	rnglidlabl.i	$⊢ I = R ↾_{𝑠} U$
Assertion	rnglidlrng	$⊢ (R \in Rng \land U \in L \land U \in SubGrp (R)) \to I \in Rng$

Proof

Step	Hyp	Ref	Expression
1		rnglidlabl.l	$⊢ L = LIdeal (R)$
2		rnglidlabl.i	$⊢ I = R ↾_{𝑠} U$
3		rngabl	$⊢ R \in Rng \to R \in Abel$
4	3	3ad2ant1	$⊢ (R \in Rng \land U \in L \land U \in SubGrp (R)) \to R \in Abel$
5		simp3	$⊢ (R \in Rng \land U \in L \land U \in SubGrp (R)) \to U \in SubGrp (R)$
6	2	subgabl	$⊢ (R \in Abel \land U \in SubGrp (R)) \to I \in Abel$
7	4 5 6	syl2anc	$⊢ (R \in Rng \land U \in L \land U \in SubGrp (R)) \to I \in Abel$
8		eqid	$⊢ 0_{R} = 0_{R}$
9	8	subg0cl	$⊢ U \in SubGrp (R) \to 0_{R} \in U$
10	1 2 8	rnglidlmsgrp	Could not format ( ( R e. Rng /\ U e. L /\ ( 0g ` R ) e. U ) -> ( mulGrp ` I ) e. Smgrp ) : No typesetting found for \|- ( ( R e. Rng /\ U e. L /\ ( 0g ` R ) e. U ) -> ( mulGrp ` I ) e. Smgrp ) with typecode \|-
11	9 10	syl3an3	Could not format ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) -> ( mulGrp ` I ) e. Smgrp ) : No typesetting found for \|- ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) -> ( mulGrp ` I ) e. Smgrp ) with typecode \|-
12		simpl1	$⊢ ((R \in Rng \land U \in L \land U \in SubGrp (R)) \land (a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I})) \to R \in Rng$
13	1 2	lidlssbas	$⊢ U \in L \to {Base}_{I} \subseteq {Base}_{R}$
14	13	sseld	$⊢ U \in L \to (a \in {Base}_{I} \to a \in {Base}_{R})$
15	13	sseld	$⊢ U \in L \to (b \in {Base}_{I} \to b \in {Base}_{R})$
16	13	sseld	$⊢ U \in L \to (c \in {Base}_{I} \to c \in {Base}_{R})$
17	14 15 16	3anim123d	$⊢ U \in L \to ((a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I}) \to (a \in {Base}_{R} \land b \in {Base}_{R} \land c \in {Base}_{R}))$
18	17	3ad2ant2	$⊢ (R \in Rng \land U \in L \land U \in SubGrp (R)) \to ((a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I}) \to (a \in {Base}_{R} \land b \in {Base}_{R} \land c \in {Base}_{R}))$
19	18	imp	$⊢ ((R \in Rng \land U \in L \land U \in SubGrp (R)) \land (a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I})) \to (a \in {Base}_{R} \land b \in {Base}_{R} \land c \in {Base}_{R})$
20		eqid	$⊢ {Base}_{R} = {Base}_{R}$
21		eqid	$⊢ +_{R} = +_{R}$
22		eqid	$⊢ \cdot_{R} = \cdot_{R}$
23	20 21 22	rngdi	$⊢ (R \in Rng \land (a \in {Base}_{R} \land b \in {Base}_{R} \land c \in {Base}_{R})) \to a \cdot_{R} (b +_{R} c) = (a \cdot_{R} b) +_{R} (a \cdot_{R} c)$
24	12 19 23	syl2anc	$⊢ ((R \in Rng \land U \in L \land U \in SubGrp (R)) \land (a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I})) \to a \cdot_{R} (b +_{R} c) = (a \cdot_{R} b) +_{R} (a \cdot_{R} c)$
25	20 21 22	rngdir	$⊢ (R \in Rng \land (a \in {Base}_{R} \land b \in {Base}_{R} \land c \in {Base}_{R})) \to (a +_{R} b) \cdot_{R} c = (a \cdot_{R} c) +_{R} (b \cdot_{R} c)$
26	12 19 25	syl2anc	$⊢ ((R \in Rng \land U \in L \land U \in SubGrp (R)) \land (a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I})) \to (a +_{R} b) \cdot_{R} c = (a \cdot_{R} c) +_{R} (b \cdot_{R} c)$
27	2 22	ressmulr	$⊢ U \in L \to \cdot_{R} = \cdot_{I}$
28	27	eqcomd	$⊢ U \in L \to \cdot_{I} = \cdot_{R}$
29		eqidd	$⊢ U \in L \to a = a$
30	2 21	ressplusg	$⊢ U \in L \to +_{R} = +_{I}$
31	30	eqcomd	$⊢ U \in L \to +_{I} = +_{R}$
32	31	oveqd	$⊢ U \in L \to b +_{I} c = b +_{R} c$
33	28 29 32	oveq123d	$⊢ U \in L \to a \cdot_{I} (b +_{I} c) = a \cdot_{R} (b +_{R} c)$
34	28	oveqd	$⊢ U \in L \to a \cdot_{I} b = a \cdot_{R} b$
35	28	oveqd	$⊢ U \in L \to a \cdot_{I} c = a \cdot_{R} c$
36	31 34 35	oveq123d	$⊢ U \in L \to (a \cdot_{I} b) +_{I} (a \cdot_{I} c) = (a \cdot_{R} b) +_{R} (a \cdot_{R} c)$
37	33 36	eqeq12d	$⊢ U \in L \to (a \cdot_{I} (b +_{I} c) = (a \cdot_{I} b) +_{I} (a \cdot_{I} c) \leftrightarrow a \cdot_{R} (b +_{R} c) = (a \cdot_{R} b) +_{R} (a \cdot_{R} c))$
38	31	oveqd	$⊢ U \in L \to a +_{I} b = a +_{R} b$
39		eqidd	$⊢ U \in L \to c = c$
40	28 38 39	oveq123d	$⊢ U \in L \to (a +_{I} b) \cdot_{I} c = (a +_{R} b) \cdot_{R} c$
41	28	oveqd	$⊢ U \in L \to b \cdot_{I} c = b \cdot_{R} c$
42	31 35 41	oveq123d	$⊢ U \in L \to (a \cdot_{I} c) +_{I} (b \cdot_{I} c) = (a \cdot_{R} c) +_{R} (b \cdot_{R} c)$
43	40 42	eqeq12d	$⊢ U \in L \to ((a +_{I} b) \cdot_{I} c = (a \cdot_{I} c) +_{I} (b \cdot_{I} c) \leftrightarrow (a +_{R} b) \cdot_{R} c = (a \cdot_{R} c) +_{R} (b \cdot_{R} c))$
44	37 43	anbi12d	$⊢ U \in L \to ((a \cdot_{I} (b +_{I} c) = (a \cdot_{I} b) +_{I} (a \cdot_{I} c) \land (a +_{I} b) \cdot_{I} c = (a \cdot_{I} c) +_{I} (b \cdot_{I} c)) \leftrightarrow (a \cdot_{R} (b +_{R} c) = (a \cdot_{R} b) +_{R} (a \cdot_{R} c) \land (a +_{R} b) \cdot_{R} c = (a \cdot_{R} c) +_{R} (b \cdot_{R} c)))$
45	44	3ad2ant2	$⊢ (R \in Rng \land U \in L \land U \in SubGrp (R)) \to ((a \cdot_{I} (b +_{I} c) = (a \cdot_{I} b) +_{I} (a \cdot_{I} c) \land (a +_{I} b) \cdot_{I} c = (a \cdot_{I} c) +_{I} (b \cdot_{I} c)) \leftrightarrow (a \cdot_{R} (b +_{R} c) = (a \cdot_{R} b) +_{R} (a \cdot_{R} c) \land (a +_{R} b) \cdot_{R} c = (a \cdot_{R} c) +_{R} (b \cdot_{R} c)))$
46	45	adantr	$⊢ ((R \in Rng \land U \in L \land U \in SubGrp (R)) \land (a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I})) \to ((a \cdot_{I} (b +_{I} c) = (a \cdot_{I} b) +_{I} (a \cdot_{I} c) \land (a +_{I} b) \cdot_{I} c = (a \cdot_{I} c) +_{I} (b \cdot_{I} c)) \leftrightarrow (a \cdot_{R} (b +_{R} c) = (a \cdot_{R} b) +_{R} (a \cdot_{R} c) \land (a +_{R} b) \cdot_{R} c = (a \cdot_{R} c) +_{R} (b \cdot_{R} c)))$
47	24 26 46	mpbir2and	$⊢ ((R \in Rng \land U \in L \land U \in SubGrp (R)) \land (a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I})) \to (a \cdot_{I} (b +_{I} c) = (a \cdot_{I} b) +_{I} (a \cdot_{I} c) \land (a +_{I} b) \cdot_{I} c = (a \cdot_{I} c) +_{I} (b \cdot_{I} c))$
48	47	ralrimivvva	$⊢ (R \in Rng \land U \in L \land U \in SubGrp (R)) \to \forall a \in {Base}_{I} \forall b \in {Base}_{I} \forall c \in {Base}_{I} (a \cdot_{I} (b +_{I} c) = (a \cdot_{I} b) +_{I} (a \cdot_{I} c) \land (a +_{I} b) \cdot_{I} c = (a \cdot_{I} c) +_{I} (b \cdot_{I} c))$
49		eqid	$⊢ {Base}_{I} = {Base}_{I}$
50		eqid	$⊢ {mulGrp}_{I} = {mulGrp}_{I}$
51		eqid	$⊢ +_{I} = +_{I}$
52		eqid	$⊢ \cdot_{I} = \cdot_{I}$
53	49 50 51 52	isrng	Could not format ( I e. Rng <-> ( I e. Abel /\ ( mulGrp ` I ) e. Smgrp /\ A. a e. ( Base ` I ) A. b e. ( Base ` I ) A. c e. ( Base ` I ) ( ( a ( .r ` I ) ( b ( +g ` I ) c ) ) = ( ( a ( .r ` I ) b ) ( +g ` I ) ( a ( .r ` I ) c ) ) /\ ( ( a ( +g ` I ) b ) ( .r ` I ) c ) = ( ( a ( .r ` I ) c ) ( +g ` I ) ( b ( .r ` I ) c ) ) ) ) ) : No typesetting found for \|- ( I e. Rng <-> ( I e. Abel /\ ( mulGrp ` I ) e. Smgrp /\ A. a e. ( Base ` I ) A. b e. ( Base ` I ) A. c e. ( Base ` I ) ( ( a ( .r ` I ) ( b ( +g ` I ) c ) ) = ( ( a ( .r ` I ) b ) ( +g ` I ) ( a ( .r ` I ) c ) ) /\ ( ( a ( +g ` I ) b ) ( .r ` I ) c ) = ( ( a ( .r ` I ) c ) ( +g ` I ) ( b ( .r ` I ) c ) ) ) ) ) with typecode \|-
54	7 11 48 53	syl3anbrc	$⊢ (R \in Rng \land U \in L \land U \in SubGrp (R)) \to I \in Rng$

Metamath Proof Explorer

Theorem rnglidlrng

Proof