Metamath Proof Explorer

Theorem 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 
|- .0. = ( 0g ` R )
rnglidlmcl.b 
|- B = ( Base ` R )
rnglidlmcl.t 
|- .x. = ( .r ` R )
rnglidlmcl.u 
|- U = ( LIdeal ` R )
Assertion rnglidlmcl 
|- ( ( ( R e. Rng /\ I e. U /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( X .x. Y ) e. I )

Proof

Step Hyp Ref Expression
1 rnglidlmcl.z 
 |-  .0. = ( 0g ` R )
2 rnglidlmcl.b 
 |-  B = ( Base ` R )
3 rnglidlmcl.t 
 |-  .x. = ( .r ` R )
4 rnglidlmcl.u 
 |-  U = ( LIdeal ` R )
5 eqid 
 |-  ( +g ` R ) = ( +g ` R )
6 4 2 5 3 islidl 
 |-  ( I e. U <-> ( I C_ B /\ I =/= (/) /\ A. x e. B A. a e. I A. b e. I ( ( x .x. a ) ( +g ` R ) b ) e. I ) )
7 oveq1 
 |-  ( x = X -> ( x .x. a ) = ( X .x. a ) )
8 7 oveq1d 
 |-  ( x = X -> ( ( x .x. a ) ( +g ` R ) b ) = ( ( X .x. a ) ( +g ` R ) b ) )
9 8 eleq1d 
 |-  ( x = X -> ( ( ( x .x. a ) ( +g ` R ) b ) e. I <-> ( ( X .x. a ) ( +g ` R ) b ) e. I ) )
10 9 ralbidv 
 |-  ( x = X -> ( A. b e. I ( ( x .x. a ) ( +g ` R ) b ) e. I <-> A. b e. I ( ( X .x. a ) ( +g ` R ) b ) e. I ) )
11 oveq2 
 |-  ( a = Y -> ( X .x. a ) = ( X .x. Y ) )
12 11 oveq1d 
 |-  ( a = Y -> ( ( X .x. a ) ( +g ` R ) b ) = ( ( X .x. Y ) ( +g ` R ) b ) )
13 12 eleq1d 
 |-  ( a = Y -> ( ( ( X .x. a ) ( +g ` R ) b ) e. I <-> ( ( X .x. Y ) ( +g ` R ) b ) e. I ) )
14 13 ralbidv 
 |-  ( a = Y -> ( A. b e. I ( ( X .x. a ) ( +g ` R ) b ) e. I <-> A. b e. I ( ( X .x. Y ) ( +g ` R ) b ) e. I ) )
15 10 14 rspc2v 
 |-  ( ( X e. B /\ Y e. I ) -> ( A. x e. B A. a e. I A. b e. I ( ( x .x. a ) ( +g ` R ) b ) e. I -> A. b e. I ( ( X .x. Y ) ( +g ` R ) b ) e. I ) )
16 15 adantl 
 |-  ( ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( A. x e. B A. a e. I A. b e. I ( ( x .x. a ) ( +g ` R ) b ) e. I -> A. b e. I ( ( X .x. Y ) ( +g ` R ) b ) e. I ) )
17 oveq2 
 |-  ( b = .0. -> ( ( X .x. Y ) ( +g ` R ) b ) = ( ( X .x. Y ) ( +g ` R ) .0. ) )
18 17 eleq1d 
 |-  ( b = .0. -> ( ( ( X .x. Y ) ( +g ` R ) b ) e. I <-> ( ( X .x. Y ) ( +g ` R ) .0. ) e. I ) )
19 18 rspcv 
 |-  ( .0. e. I -> ( A. b e. I ( ( X .x. Y ) ( +g ` R ) b ) e. I -> ( ( X .x. Y ) ( +g ` R ) .0. ) e. I ) )
20 19 adantl 
 |-  ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) -> ( A. b e. I ( ( X .x. Y ) ( +g ` R ) b ) e. I -> ( ( X .x. Y ) ( +g ` R ) .0. ) e. I ) )
21 rnggrp 
 |-  ( R e. Rng -> R e. Grp )
22 21 3ad2ant1 
 |-  ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) -> R e. Grp )
23 22 adantr 
 |-  ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) -> R e. Grp )
24 23 adantr 
 |-  ( ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> R e. Grp )
25 simpll1 
 |-  ( ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> R e. Rng )
26 simprl 
 |-  ( ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> X e. B )
27 ssel 
 |-  ( I C_ B -> ( Y e. I -> Y e. B ) )
28 27 3ad2ant2 
 |-  ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) -> ( Y e. I -> Y e. B ) )
29 28 adantr 
 |-  ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) -> ( Y e. I -> Y e. B ) )
30 29 adantld 
 |-  ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) -> ( ( X e. B /\ Y e. I ) -> Y e. B ) )
31 30 imp 
 |-  ( ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> Y e. B )
32 2 3 rngcl 
 |-  ( ( R e. Rng /\ X e. B /\ Y e. B ) -> ( X .x. Y ) e. B )
33 25 26 31 32 syl3anc 
 |-  ( ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( X .x. Y ) e. B )
34 2 5 1 24 33 grpridd 
 |-  ( ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( ( X .x. Y ) ( +g ` R ) .0. ) = ( X .x. Y ) )
35 34 eleq1d 
 |-  ( ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( ( ( X .x. Y ) ( +g ` R ) .0. ) e. I <-> ( X .x. Y ) e. I ) )
36 35 biimpd 
 |-  ( ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( ( ( X .x. Y ) ( +g ` R ) .0. ) e. I -> ( X .x. Y ) e. I ) )
37 36 ex 
 |-  ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) -> ( ( X e. B /\ Y e. I ) -> ( ( ( X .x. Y ) ( +g ` R ) .0. ) e. I -> ( X .x. Y ) e. I ) ) )
38 20 37 syl5d 
 |-  ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) -> ( ( X e. B /\ Y e. I ) -> ( A. b e. I ( ( X .x. Y ) ( +g ` R ) b ) e. I -> ( X .x. Y ) e. I ) ) )
39 38 imp 
 |-  ( ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( A. b e. I ( ( X .x. Y ) ( +g ` R ) b ) e. I -> ( X .x. Y ) e. I ) )
40 16 39 syld 
 |-  ( ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( A. x e. B A. a e. I A. b e. I ( ( x .x. a ) ( +g ` R ) b ) e. I -> ( X .x. Y ) e. I ) )
41 40 ex 
 |-  ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) -> ( ( X e. B /\ Y e. I ) -> ( A. x e. B A. a e. I A. b e. I ( ( x .x. a ) ( +g ` R ) b ) e. I -> ( X .x. Y ) e. I ) ) )
42 41 com23 
 |-  ( ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) /\ .0. e. I ) -> ( A. x e. B A. a e. I A. b e. I ( ( x .x. a ) ( +g ` R ) b ) e. I -> ( ( X e. B /\ Y e. I ) -> ( X .x. Y ) e. I ) ) )
43 42 ex 
 |-  ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) -> ( .0. e. I -> ( A. x e. B A. a e. I A. b e. I ( ( x .x. a ) ( +g ` R ) b ) e. I -> ( ( X e. B /\ Y e. I ) -> ( X .x. Y ) e. I ) ) ) )
44 43 com23 
 |-  ( ( R e. Rng /\ I C_ B /\ I =/= (/) ) -> ( A. x e. B A. a e. I A. b e. I ( ( x .x. a ) ( +g ` R ) b ) e. I -> ( .0. e. I -> ( ( X e. B /\ Y e. I ) -> ( X .x. Y ) e. I ) ) ) )
45 44 3exp 
 |-  ( R e. Rng -> ( I C_ B -> ( I =/= (/) -> ( A. x e. B A. a e. I A. b e. I ( ( x .x. a ) ( +g ` R ) b ) e. I -> ( .0. e. I -> ( ( X e. B /\ Y e. I ) -> ( X .x. Y ) e. I ) ) ) ) ) )
46 45 3impd 
 |-  ( R e. Rng -> ( ( I C_ B /\ I =/= (/) /\ A. x e. B A. a e. I A. b e. I ( ( x .x. a ) ( +g ` R ) b ) e. I ) -> ( .0. e. I -> ( ( X e. B /\ Y e. I ) -> ( X .x. Y ) e. I ) ) ) )
47 6 46 biimtrid 
 |-  ( R e. Rng -> ( I e. U -> ( .0. e. I -> ( ( X e. B /\ Y e. I ) -> ( X .x. Y ) e. I ) ) ) )
48 47 3imp1 
 |-  ( ( ( R e. Rng /\ I e. U /\ .0. e. I ) /\ ( X e. B /\ Y e. I ) ) -> ( X .x. Y ) e. I )