Metamath Proof Explorer

Theorem idlsrg0g

Description: The zero ideal is the additive identity of the semiring of ideals. (Contributed by Thierry Arnoux, 1-Jun-2024)

Ref Expression
Hypotheses idlsrg0g.1 
|- S = ( IDLsrg ` R )
idlsrg0g.2 
|- .0. = ( 0g ` R )
Assertion idlsrg0g 
|- ( R e. Ring -> { .0. } = ( 0g ` S ) )

Proof

Step Hyp Ref Expression
1 idlsrg0g.1 
 |-  S = ( IDLsrg ` R )
2 idlsrg0g.2 
 |-  .0. = ( 0g ` R )
3 eqid 
 |-  ( Base ` S ) = ( Base ` S )
4 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
5 eqid 
 |-  ( +g ` S ) = ( +g ` S )
6 eqid 
 |-  ( LIdeal ` R ) = ( LIdeal ` R )
7 6 2 lidl0 
 |-  ( R e. Ring -> { .0. } e. ( LIdeal ` R ) )
8 1 6 idlsrgbas 
 |-  ( R e. Ring -> ( LIdeal ` R ) = ( Base ` S ) )
9 7 8 eleqtrd 
 |-  ( R e. Ring -> { .0. } e. ( Base ` S ) )
10 eqid 
 |-  ( LSSum ` R ) = ( LSSum ` R )
11 1 10 idlsrgplusg 
 |-  ( R e. Ring -> ( LSSum ` R ) = ( +g ` S ) )
12 11 adantr 
 |-  ( ( R e. Ring /\ i e. ( Base ` S ) ) -> ( LSSum ` R ) = ( +g ` S ) )
13 12 oveqd 
 |-  ( ( R e. Ring /\ i e. ( Base ` S ) ) -> ( { .0. } ( LSSum ` R ) i ) = ( { .0. } ( +g ` S ) i ) )
14 simpr 
 |-  ( ( R e. Ring /\ i e. ( Base ` S ) ) -> i e. ( Base ` S ) )
15 8 adantr 
 |-  ( ( R e. Ring /\ i e. ( Base ` S ) ) -> ( LIdeal ` R ) = ( Base ` S ) )
16 14 15 eleqtrrd 
 |-  ( ( R e. Ring /\ i e. ( Base ` S ) ) -> i e. ( LIdeal ` R ) )
17 6 lidlsubg 
 |-  ( ( R e. Ring /\ i e. ( LIdeal ` R ) ) -> i e. ( SubGrp ` R ) )
18 16 17 syldan 
 |-  ( ( R e. Ring /\ i e. ( Base ` S ) ) -> i e. ( SubGrp ` R ) )
19 2 10 lsm02 
 |-  ( i e. ( SubGrp ` R ) -> ( { .0. } ( LSSum ` R ) i ) = i )
20 18 19 syl 
 |-  ( ( R e. Ring /\ i e. ( Base ` S ) ) -> ( { .0. } ( LSSum ` R ) i ) = i )
21 13 20 eqtr3d 
 |-  ( ( R e. Ring /\ i e. ( Base ` S ) ) -> ( { .0. } ( +g ` S ) i ) = i )
22 12 oveqd 
 |-  ( ( R e. Ring /\ i e. ( Base ` S ) ) -> ( i ( LSSum ` R ) { .0. } ) = ( i ( +g ` S ) { .0. } ) )
23 2 10 lsm01 
 |-  ( i e. ( SubGrp ` R ) -> ( i ( LSSum ` R ) { .0. } ) = i )
24 18 23 syl 
 |-  ( ( R e. Ring /\ i e. ( Base ` S ) ) -> ( i ( LSSum ` R ) { .0. } ) = i )
25 22 24 eqtr3d 
 |-  ( ( R e. Ring /\ i e. ( Base ` S ) ) -> ( i ( +g ` S ) { .0. } ) = i )
26 3 4 5 9 21 25 ismgmid2 
 |-  ( R e. Ring -> { .0. } = ( 0g ` S ) )