Metamath Proof Explorer

Theorem intlidl

Description: The intersection of a nonempty collection of ideals is an ideal. (Contributed by Thierry Arnoux, 8-Jun-2024)

Ref Expression
Assertion intlidl 
|- ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> |^| C e. ( LIdeal ` R ) )

Proof

Step Hyp Ref Expression
1 simp3 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> C C_ ( LIdeal ` R ) )
2 1 sselda 
 |-  ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ i e. C ) -> i e. ( LIdeal ` R ) )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
5 3 4 lidlss 
 |-  ( i e. ( LIdeal ` R ) -> i C_ ( Base ` R ) )
6 2 5 syl 
 |-  ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ i e. C ) -> i C_ ( Base ` R ) )
7 6 ralrimiva 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> A. i e. C i C_ ( Base ` R ) )
8 pwssb 
 |-  ( C C_ ~P ( Base ` R ) <-> A. i e. C i C_ ( Base ` R ) )
9 7 8 sylibr 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> C C_ ~P ( Base ` R ) )
10 simp2 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> C =/= (/) )
11 intss2 
 |-  ( C C_ ~P ( Base ` R ) -> ( C =/= (/) -> |^| C C_ ( Base ` R ) ) )
12 11 imp 
 |-  ( ( C C_ ~P ( Base ` R ) /\ C =/= (/) ) -> |^| C C_ ( Base ` R ) )
13 9 10 12 syl2anc 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> |^| C C_ ( Base ` R ) )
14 simpl1 
 |-  ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ i e. C ) -> R e. Ring )
15 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
16 4 15 lidl0cl 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) -> ( 0g ` R ) e. i )
17 14 2 16 syl2anc 
 |-  ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ i e. C ) -> ( 0g ` R ) e. i )
18 17 ralrimiva 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> A. i e. C ( 0g ` R ) e. i )
19 fvex 
 |-  ( 0g ` R ) e. _V
20 19 elint2 
 |-  ( ( 0g ` R ) e. |^| C <-> A. i e. C ( 0g ` R ) e. i )
21 18 20 sylibr 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> ( 0g ` R ) e. |^| C )
22 21 ne0d 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> |^| C =/= (/) )
23 14 ad5ant15 
 |-  ( ( ( ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ a e. |^| C ) /\ b e. |^| C ) /\ i e. C ) -> R e. Ring )
24 2 ad5ant15 
 |-  ( ( ( ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ a e. |^| C ) /\ b e. |^| C ) /\ i e. C ) -> i e. ( LIdeal ` R ) )
25 simp-4r 
 |-  ( ( ( ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ a e. |^| C ) /\ b e. |^| C ) /\ i e. C ) -> x e. ( Base ` R ) )
26 simpllr 
 |-  ( ( ( ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ a e. |^| C ) /\ b e. |^| C ) /\ i e. C ) -> a e. |^| C )
27 simpr 
 |-  ( ( ( ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ a e. |^| C ) /\ b e. |^| C ) /\ i e. C ) -> i e. C )
28 elinti 
 |-  ( a e. |^| C -> ( i e. C -> a e. i ) )
29 28 imp 
 |-  ( ( a e. |^| C /\ i e. C ) -> a e. i )
30 26 27 29 syl2anc 
 |-  ( ( ( ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ a e. |^| C ) /\ b e. |^| C ) /\ i e. C ) -> a e. i )
31 eqid 
 |-  ( .r ` R ) = ( .r ` R )
32 4 3 31 lidlmcl 
 |-  ( ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) /\ ( x e. ( Base ` R ) /\ a e. i ) ) -> ( x ( .r ` R ) a ) e. i )
33 23 24 25 30 32 syl22anc 
 |-  ( ( ( ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ a e. |^| C ) /\ b e. |^| C ) /\ i e. C ) -> ( x ( .r ` R ) a ) e. i )
34 elinti 
 |-  ( b e. |^| C -> ( i e. C -> b e. i ) )
35 34 imp 
 |-  ( ( b e. |^| C /\ i e. C ) -> b e. i )
36 35 adantll 
 |-  ( ( ( ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ a e. |^| C ) /\ b e. |^| C ) /\ i e. C ) -> b e. i )
37 eqid 
 |-  ( +g ` R ) = ( +g ` R )
38 4 37 lidlacl 
 |-  ( ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) /\ ( ( x ( .r ` R ) a ) e. i /\ b e. i ) ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i )
39 23 24 33 36 38 syl22anc 
 |-  ( ( ( ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ a e. |^| C ) /\ b e. |^| C ) /\ i e. C ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i )
40 39 ralrimiva 
 |-  ( ( ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ a e. |^| C ) /\ b e. |^| C ) -> A. i e. C ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i )
41 ovex 
 |-  ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. _V
42 41 elint2 
 |-  ( ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. |^| C <-> A. i e. C ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. i )
43 40 42 sylibr 
 |-  ( ( ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ a e. |^| C ) /\ b e. |^| C ) -> ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. |^| C )
44 43 ralrimiva 
 |-  ( ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ x e. ( Base ` R ) ) /\ a e. |^| C ) -> A. b e. |^| C ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. |^| C )
45 44 anasss 
 |-  ( ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) /\ ( x e. ( Base ` R ) /\ a e. |^| C ) ) -> A. b e. |^| C ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. |^| C )
46 45 ralrimivva 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> A. x e. ( Base ` R ) A. a e. |^| C A. b e. |^| C ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. |^| C )
47 4 3 37 31 islidl 
 |-  ( |^| C e. ( LIdeal ` R ) <-> ( |^| C C_ ( Base ` R ) /\ |^| C =/= (/) /\ A. x e. ( Base ` R ) A. a e. |^| C A. b e. |^| C ( ( x ( .r ` R ) a ) ( +g ` R ) b ) e. |^| C ) )
48 13 22 46 47 syl3anbrc 
 |-  ( ( R e. Ring /\ C =/= (/) /\ C C_ ( LIdeal ` R ) ) -> |^| C e. ( LIdeal ` R ) )