lidlrng

Description: A (left) ideal of a ring is a non-unital ring. (Contributed by AV, 17-Feb-2020)

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

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	$⊢ L = LIdeal (R)$
2		lidlabl.i	$⊢ I = R ↾_{𝑠} U$
3	1 2	lidlabl	$⊢ (R \in Ring \land U \in L) \to I \in Abel$
4	1 2	lidlmsgrp	Could not format ( ( R e. Ring /\ U e. L ) -> ( mulGrp ` I ) e. Smgrp ) : No typesetting found for \|- ( ( R e. Ring /\ U e. L ) -> ( mulGrp ` I ) e. Smgrp ) with typecode \|-
5		simpll	$⊢ ((R \in Ring \land U \in L) \land (a \in {Base}_{I} \land b \in {Base}_{I} \land c \in {Base}_{I})) \to R \in Ring$
6	1 2	lidlssbas	$⊢ U \in L \to {Base}_{I} \subseteq {Base}_{R}$
7	6	sseld	$⊢ U \in L \to (a \in {Base}_{I} \to a \in {Base}_{R})$
8	6	sseld	$⊢ U \in L \to (b \in {Base}_{I} \to b \in {Base}_{R})$
9	6	sseld	$⊢ U \in L \to (c \in {Base}_{I} \to c \in {Base}_{R})$
10	7 8 9	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}))$
11	10	adantl	$⊢ (R \in Ring \land 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}))$
12	11	imp	$⊢ ((R \in Ring \land U \in L) \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})$
13		eqid	$⊢ {Base}_{R} = {Base}_{R}$
14		eqid	$⊢ +_{R} = +_{R}$
15		eqid	$⊢ \cdot_{R} = \cdot_{R}$
16	13 14 15	ringdi	$⊢ (R \in Ring \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)$
17	5 12 16	syl2anc	$⊢ ((R \in Ring \land U \in L) \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)$
18	13 14 15	ringdir	$⊢ (R \in Ring \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)$
19	5 12 18	syl2anc	$⊢ ((R \in Ring \land U \in L) \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)$
20	17 19	jca	$⊢ ((R \in Ring \land U \in L) \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) \land (a +_{R} b) \cdot_{R} c = (a \cdot_{R} c) +_{R} (b \cdot_{R} c))$
21	20	ralrimivvva	$⊢ (R \in Ring \land U \in L) \to \forall a \in {Base}_{I} \forall b \in {Base}_{I} \forall c \in {Base}_{I} (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))$
22	2 15	ressmulr	$⊢ U \in L \to \cdot_{R} = \cdot_{I}$
23	22	eqcomd	$⊢ U \in L \to \cdot_{I} = \cdot_{R}$
24		eqidd	$⊢ U \in L \to a = a$
25	2 14	ressplusg	$⊢ U \in L \to +_{R} = +_{I}$
26	25	eqcomd	$⊢ U \in L \to +_{I} = +_{R}$
27	26	oveqd	$⊢ U \in L \to b +_{I} c = b +_{R} c$
28	23 24 27	oveq123d	$⊢ U \in L \to a \cdot_{I} (b +_{I} c) = a \cdot_{R} (b +_{R} c)$
29	23	oveqd	$⊢ U \in L \to a \cdot_{I} b = a \cdot_{R} b$
30	23	oveqd	$⊢ U \in L \to a \cdot_{I} c = a \cdot_{R} c$
31	26 29 30	oveq123d	$⊢ U \in L \to (a \cdot_{I} b) +_{I} (a \cdot_{I} c) = (a \cdot_{R} b) +_{R} (a \cdot_{R} c)$
32	28 31	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))$
33	26	oveqd	$⊢ U \in L \to a +_{I} b = a +_{R} b$
34		eqidd	$⊢ U \in L \to c = c$
35	23 33 34	oveq123d	$⊢ U \in L \to (a +_{I} b) \cdot_{I} c = (a +_{R} b) \cdot_{R} c$
36	23	oveqd	$⊢ U \in L \to b \cdot_{I} c = b \cdot_{R} c$
37	26 30 36	oveq123d	$⊢ U \in L \to (a \cdot_{I} c) +_{I} (b \cdot_{I} c) = (a \cdot_{R} c) +_{R} (b \cdot_{R} c)$
38	35 37	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))$
39	32 38	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)))$
40	39	adantl	$⊢ (R \in Ring \land 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)))$
41	40	ralbidv	$⊢ (R \in Ring \land U \in L) \to (\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)) \leftrightarrow \forall c \in {Base}_{I} (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)))$
42	41	2ralbidv	$⊢ (R \in Ring \land U \in L) \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)) \leftrightarrow \forall a \in {Base}_{I} \forall b \in {Base}_{I} \forall c \in {Base}_{I} (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)))$
43	21 42	mpbird	$⊢ (R \in Ring \land U \in L) \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))$
44		eqid	$⊢ {Base}_{I} = {Base}_{I}$
45		eqid	$⊢ {mulGrp}_{I} = {mulGrp}_{I}$
46		eqid	$⊢ +_{I} = +_{I}$
47		eqid	$⊢ \cdot_{I} = \cdot_{I}$
48	44 45 46 47	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 \|-
49	3 4 43 48	syl3anbrc	$⊢ (R \in Ring \land U \in L) \to I \in Rng$

Metamath Proof Explorer

Theorem lidlrng

Proof