Metamath Proof Explorer

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

Proof

Step Hyp Ref Expression
1 rnglidlabl.l 
 |-  L = ( LIdeal ` R )
2 rnglidlabl.i 
 |-  I = ( R |`s U )
3 rngabl 
 |-  ( R e. Rng -> R e. Abel )
4 3 3ad2ant1 
 |-  ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) -> R e. Abel )
5 simp3 
 |-  ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) -> U e. ( SubGrp ` R ) )
6 2 subgabl 
 |-  ( ( R e. Abel /\ U e. ( SubGrp ` R ) ) -> I e. Abel )
7 4 5 6 syl2anc 
 |-  ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) -> I e. Abel )
8 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 8 subg0cl 
 |-  ( U e. ( SubGrp ` R ) -> ( 0g ` R ) e. U )
10 1 2 8 rnglidlmsgrp 
 |-  ( ( R e. Rng /\ U e. L /\ ( 0g ` R ) e. U ) -> ( mulGrp ` I ) e. Smgrp )
11 9 10 syl3an3 
 |-  ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) -> ( mulGrp ` I ) e. Smgrp )
12 simpl1 
 |-  ( ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) ) -> R e. Rng )
13 1 2 lidlssbas 
 |-  ( U e. L -> ( Base ` I ) C_ ( Base ` R ) )
14 13 sseld 
 |-  ( U e. L -> ( a e. ( Base ` I ) -> a e. ( Base ` R ) ) )
15 13 sseld 
 |-  ( U e. L -> ( b e. ( Base ` I ) -> b e. ( Base ` R ) ) )
16 13 sseld 
 |-  ( U e. L -> ( c e. ( Base ` I ) -> c e. ( Base ` R ) ) )
17 14 15 16 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 ) ) ) )
18 17 3ad2ant2 
 |-  ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) -> ( ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) /\ c e. ( Base ` R ) ) ) )
19 18 imp 
 |-  ( ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ c e. ( Base ` I ) ) ) -> ( a e. ( Base ` R ) /\ b e. ( Base ` R ) /\ c e. ( Base ` R ) ) )
20 eqid 
 |-  ( Base ` R ) = ( Base ` R )
21 eqid 
 |-  ( +g ` R ) = ( +g ` R )
22 eqid 
 |-  ( .r ` R ) = ( .r ` R )
23 20 21 22 rngdi 
 |-  ( ( R e. Rng /\ ( 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 ) ) )
24 12 19 23 syl2anc 
 |-  ( ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) /\ ( 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 ) ) )
25 20 21 22 rngdir 
 |-  ( ( R e. Rng /\ ( 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 ) ) )
26 12 19 25 syl2anc 
 |-  ( ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) /\ ( 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 ) ) )
27 2 22 ressmulr 
 |-  ( U e. L -> ( .r ` R ) = ( .r ` I ) )
28 27 eqcomd 
 |-  ( U e. L -> ( .r ` I ) = ( .r ` R ) )
29 eqidd 
 |-  ( U e. L -> a = a )
30 2 21 ressplusg 
 |-  ( U e. L -> ( +g ` R ) = ( +g ` I ) )
31 30 eqcomd 
 |-  ( U e. L -> ( +g ` I ) = ( +g ` R ) )
32 31 oveqd 
 |-  ( U e. L -> ( b ( +g ` I ) c ) = ( b ( +g ` R ) c ) )
33 28 29 32 oveq123d 
 |-  ( U e. L -> ( a ( .r ` I ) ( b ( +g ` I ) c ) ) = ( a ( .r ` R ) ( b ( +g ` R ) c ) ) )
34 28 oveqd 
 |-  ( U e. L -> ( a ( .r ` I ) b ) = ( a ( .r ` R ) b ) )
35 28 oveqd 
 |-  ( U e. L -> ( a ( .r ` I ) c ) = ( a ( .r ` R ) c ) )
36 31 34 35 oveq123d 
 |-  ( U e. L -> ( ( a ( .r ` I ) b ) ( +g ` I ) ( a ( .r ` I ) c ) ) = ( ( a ( .r ` R ) b ) ( +g ` R ) ( a ( .r ` R ) c ) ) )
37 33 36 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 ) ) ) )
38 31 oveqd 
 |-  ( U e. L -> ( a ( +g ` I ) b ) = ( a ( +g ` R ) b ) )
39 eqidd 
 |-  ( U e. L -> c = c )
40 28 38 39 oveq123d 
 |-  ( U e. L -> ( ( a ( +g ` I ) b ) ( .r ` I ) c ) = ( ( a ( +g ` R ) b ) ( .r ` R ) c ) )
41 28 oveqd 
 |-  ( U e. L -> ( b ( .r ` I ) c ) = ( b ( .r ` R ) c ) )
42 31 35 41 oveq123d 
 |-  ( U e. L -> ( ( a ( .r ` I ) c ) ( +g ` I ) ( b ( .r ` I ) c ) ) = ( ( a ( .r ` R ) c ) ( +g ` R ) ( b ( .r ` R ) c ) ) )
43 40 42 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 ) ) ) )
44 37 43 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 ) ) ) ) )
45 44 3ad2ant2 
 |-  ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) -> ( ( ( 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 ) ) ) ) )
46 45 adantr 
 |-  ( ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ 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 ( .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 ) ) ) ) )
47 24 26 46 mpbir2and 
 |-  ( ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) /\ ( a e. ( Base ` I ) /\ b e. ( Base ` I ) /\ 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 ) ) ) )
48 47 ralrimivvva 
 |-  ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) -> 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 eqid 
 |-  ( Base ` I ) = ( Base ` I )
50 eqid 
 |-  ( mulGrp ` I ) = ( mulGrp ` I )
51 eqid 
 |-  ( +g ` I ) = ( +g ` I )
52 eqid 
 |-  ( .r ` I ) = ( .r ` I )
53 49 50 51 52 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 ) ) ) ) )
54 7 11 48 53 syl3anbrc 
 |-  ( ( R e. Rng /\ U e. L /\ U e. ( SubGrp ` R ) ) -> I e. Rng )