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 \|`s U )
Assertion	lidlrng	\|- ( ( R e. Ring /\ U e. L ) -> I e. Rng )

Proof

Step	Hyp	Ref	Expression
1		lidlabl.l	\|- L = ( LIdeal ` R )
2		lidlabl.i	\|- I = ( R \|`s U )
3	1 2	lidlabl	\|- ( ( R e. Ring /\ U e. L ) -> I e. Abel )
4	1 2	lidlmsgrp	\|- ( ( R e. Ring /\ U e. L ) -> ( mulGrp ` I ) e. Smgrp )
5		simpll	\|- ( ( ( R e. Ring /\ U e. L ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) ) -> R e. Ring )
6	1 2	lidlssbas	\|- ( U e. L -> ( Base ` I ) C_ ( Base ` R ) )
7	6	sseld	\|- ( U e. L -> ( a e. ( Base ` I ) -> a e. ( Base ` R ) ) )
8	6	sseld	\|- ( U e. L -> ( b e. ( Base ` I ) -> b e. ( Base ` R ) ) )
9	6	sseld	\|- ( U e. L -> ( c e. ( Base ` I ) -> c e. ( Base ` R ) ) )
10	7 8 9	3anim123d	\|- ( U e. L -> ( ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) /\ c e. ( Base ` R ) ) ) )
11	10	adantl	\|- ( ( R e. Ring /\ U e. L ) -> ( ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) /\ c e. ( Base ` R ) ) ) )
12	11	imp	\|- ( ( ( R e. Ring /\ U e. L ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) /\ c e. ( Base ` R ) ) )
13		eqid	\|- ( Base ` R ) = ( Base ` R )
14		eqid	\|- ( +g ` R ) = ( +g ` R )
15		eqid	\|- ( .r ` R ) = ( .r ` R )
16	13 14 15	ringdi	\|- ( ( R e. Ring /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) /\ c e. ( Base ` R ) ) ) -> ( a ( .r ` R ) ( b ( +g ` R ) c ) ) = ( ( a ( .r ` R ) b ) ( +g ` R ) ( a ( .r ` R ) c ) ) )
17	5 12 16	syl2anc	\|- ( ( ( R e. Ring /\ U e. L ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) ) -> ( a ( .r ` R ) ( b ( +g ` R ) c ) ) = ( ( a ( .r ` R ) b ) ( +g ` R ) ( a ( .r ` R ) c ) ) )
18	13 14 15	ringdir	\|- ( ( R e. Ring /\ ( a e. ( Base ` R ) /\ b e. ( Base ` R ) /\ c e. ( Base ` R ) ) ) -> ( ( a ( +g ` R ) b ) ( .r ` R ) c ) = ( ( a ( .r ` R ) c ) ( +g ` R ) ( b ( .r ` R ) c ) ) )
19	5 12 18	syl2anc	\|- ( ( ( R e. Ring /\ U e. L ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) ) -> ( ( a ( +g ` R ) b ) ( .r ` R ) c ) = ( ( a ( .r ` R ) c ) ( +g ` R ) ( b ( .r ` R ) c ) ) )
20	17 19	jca	\|- ( ( ( R e. Ring /\ U e. L ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) ) -> ( ( a ( .r ` R ) ( b ( +g ` R ) c ) ) = ( ( a ( .r ` R ) b ) ( +g ` R ) ( a ( .r ` R ) c ) ) /\ ( ( a ( +g ` R ) b ) ( .r ` R ) c ) = ( ( a ( .r ` R ) c ) ( +g ` R ) ( b ( .r ` R ) c ) ) ) )
21	20	ralrimivvva	\|- ( ( R e. Ring /\ U e. L ) -> A. a e. ( Base ` I ) A. b e. ( Base ` I ) A. c e. ( Base ` I ) ( ( a ( .r ` R ) ( b ( +g ` R ) c ) ) = ( ( a ( .r ` R ) b ) ( +g ` R ) ( a ( .r ` R ) c ) ) /\ ( ( a ( +g ` R ) b ) ( .r ` R ) c ) = ( ( a ( .r ` R ) c ) ( +g ` R ) ( b ( .r ` R ) c ) ) ) )
22	2 15	ressmulr	\|- ( U e. L -> ( .r ` R ) = ( .r ` I ) )
23	22	eqcomd	\|- ( U e. L -> ( .r ` I ) = ( .r ` R ) )
24		eqidd	\|- ( U e. L -> a = a )
25	2 14	ressplusg	\|- ( U e. L -> ( +g ` R ) = ( +g ` I ) )
26	25	eqcomd	\|- ( U e. L -> ( +g ` I ) = ( +g ` R ) )
27	26	oveqd	\|- ( U e. L -> ( b ( +g ` I ) c ) = ( b ( +g ` R ) c ) )
28	23 24 27	oveq123d	\|- ( U e. L -> ( a ( .r ` I ) ( b ( +g ` I ) c ) ) = ( a ( .r ` R ) ( b ( +g ` R ) c ) ) )
29	23	oveqd	\|- ( U e. L -> ( a ( .r ` I ) b ) = ( a ( .r ` R ) b ) )
30	23	oveqd	\|- ( U e. L -> ( a ( .r ` I ) c ) = ( a ( .r ` R ) c ) )
31	26 29 30	oveq123d	\|- ( U e. L -> ( ( a ( .r ` I ) b ) ( +g ` I ) ( a ( .r ` I ) c ) ) = ( ( a ( .r ` R ) b ) ( +g ` R ) ( a ( .r ` R ) c ) ) )
32	28 31	eqeq12d	\|- ( U e. L -> ( ( a ( .r ` I ) ( b ( +g ` I ) c ) ) = ( ( a ( .r ` I ) b ) ( +g ` I ) ( a ( .r ` I ) c ) ) <-> ( a ( .r ` R ) ( b ( +g ` R ) c ) ) = ( ( a ( .r ` R ) b ) ( +g ` R ) ( a ( .r ` R ) c ) ) ) )
33	26	oveqd	\|- ( U e. L -> ( a ( +g ` I ) b ) = ( a ( +g ` R ) b ) )
34		eqidd	\|- ( U e. L -> c = c )
35	23 33 34	oveq123d	\|- ( U e. L -> ( ( a ( +g ` I ) b ) ( .r ` I ) c ) = ( ( a ( +g ` R ) b ) ( .r ` R ) c ) )
36	23	oveqd	\|- ( U e. L -> ( b ( .r ` I ) c ) = ( b ( .r ` R ) c ) )
37	26 30 36	oveq123d	\|- ( U e. L -> ( ( a ( .r ` I ) c ) ( +g ` I ) ( b ( .r ` I ) c ) ) = ( ( a ( .r ` R ) c ) ( +g ` R ) ( b ( .r ` R ) c ) ) )
38	35 37	eqeq12d	\|- ( U e. L -> ( ( ( a ( +g ` I ) b ) ( .r ` I ) c ) = ( ( a ( .r ` I ) c ) ( +g ` I ) ( b ( .r ` I ) c ) ) <-> ( ( a ( +g ` R ) b ) ( .r ` R ) c ) = ( ( a ( .r ` R ) c ) ( +g ` R ) ( b ( .r ` R ) c ) ) ) )
39	32 38	anbi12d	\|- ( U e. L -> ( ( ( 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 ) ) ) <-> ( ( a ( .r ` R ) ( b ( +g ` R ) c ) ) = ( ( a ( .r ` R ) b ) ( +g ` R ) ( a ( .r ` R ) c ) ) /\ ( ( a ( +g ` R ) b ) ( .r ` R ) c ) = ( ( a ( .r ` R ) c ) ( +g ` R ) ( b ( .r ` R ) c ) ) ) ) )
40	39	adantl	\|- ( ( R e. Ring /\ U e. L ) -> ( ( ( 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 ) ) ) <-> ( ( a ( .r ` R ) ( b ( +g ` R ) c ) ) = ( ( a ( .r ` R ) b ) ( +g ` R ) ( a ( .r ` R ) c ) ) /\ ( ( a ( +g ` R ) b ) ( .r ` R ) c ) = ( ( a ( .r ` R ) c ) ( +g ` R ) ( b ( .r ` R ) c ) ) ) ) )
41	40	ralbidv	\|- ( ( R e. Ring /\ U e. L ) -> ( 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 ) ) ) <-> A. c e. ( Base ` I ) ( ( a ( .r ` R ) ( b ( +g ` R ) c ) ) = ( ( a ( .r ` R ) b ) ( +g ` R ) ( a ( .r ` R ) c ) ) /\ ( ( a ( +g ` R ) b ) ( .r ` R ) c ) = ( ( a ( .r ` R ) c ) ( +g ` R ) ( b ( .r ` R ) c ) ) ) ) )
42	41	2ralbidv	\|- ( ( R e. Ring /\ U e. L ) -> ( 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 ) ) ) <-> A. a e. ( Base ` I ) A. b e. ( Base ` I ) A. c e. ( Base ` I ) ( ( a ( .r ` R ) ( b ( +g ` R ) c ) ) = ( ( a ( .r ` R ) b ) ( +g ` R ) ( a ( .r ` R ) c ) ) /\ ( ( a ( +g ` R ) b ) ( .r ` R ) c ) = ( ( a ( .r ` R ) c ) ( +g ` R ) ( b ( .r ` R ) c ) ) ) ) )
43	21 42	mpbird	\|- ( ( R e. Ring /\ U e. L ) -> 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 ) ) ) )
44		eqid	\|- ( Base ` I ) = ( Base ` I )
45		eqid	\|- ( mulGrp ` I ) = ( mulGrp ` I )
46		eqid	\|- ( +g ` I ) = ( +g ` I )
47		eqid	\|- ( .r ` I ) = ( .r ` I )
48	44 45 46 47	isrng	\|- ( 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 ) ) ) ) )
49	3 4 43 48	syl3anbrc	\|- ( ( R e. Ring /\ U e. L ) -> I e. Rng )

Metamath Proof Explorer

Theorem lidlrng

Proof