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 ˙ = 0 R
Assertion idlsrg0g ⊢ R ∈ Ring → 0 ˙ = 0 S

Proof

Step Hyp Ref Expression
1 idlsrg0g.1 ⊢ S = IDLsrg ⁡ R
2 idlsrg0g.2 ⊢ 0 ˙ = 0 R
3 eqid ⊢ Base S = Base S
4 eqid ⊢ 0 S = 0 S
5 eqid ⊢ + S = + S
6 eqid ⊢ LIdeal ⁡ R = LIdeal ⁡ R
7 6 2 lidl0 ⊢ R ∈ Ring → 0 ˙ ∈ LIdeal ⁡ R
8 1 6 idlsrgbas ⊢ R ∈ Ring → LIdeal ⁡ R = Base S
9 7 8 eleqtrd ⊢ R ∈ Ring → 0 ˙ ∈ Base S
10 eqid ⊢ LSSum ⁡ R = LSSum ⁡ R
11 1 10 idlsrgplusg ⊢ R ∈ Ring → LSSum ⁡ R = + S
12 11 adantr ⊢ R ∈ Ring ∧ i ∈ Base S → LSSum ⁡ R = + S
13 12 oveqd ⊢ R ∈ Ring ∧ i ∈ Base S → 0 ˙ LSSum ⁡ R i = 0 ˙ + S i
14 simpr ⊢ R ∈ Ring ∧ i ∈ Base S → i ∈ Base S
15 8 adantr ⊢ R ∈ Ring ∧ i ∈ Base S → LIdeal ⁡ R = Base S
16 14 15 eleqtrrd ⊢ R ∈ Ring ∧ i ∈ Base S → i ∈ LIdeal ⁡ R
17 6 lidlsubg ⊢ R ∈ Ring ∧ i ∈ LIdeal ⁡ R → i ∈ SubGrp ⁡ R
18 16 17 syldan ⊢ R ∈ Ring ∧ i ∈ Base S → i ∈ SubGrp ⁡ R
19 2 10 lsm02 ⊢ i ∈ SubGrp ⁡ R → 0 ˙ LSSum ⁡ R i = i
20 18 19 syl ⊢ R ∈ Ring ∧ i ∈ Base S → 0 ˙ LSSum ⁡ R i = i
21 13 20 eqtr3d ⊢ R ∈ Ring ∧ i ∈ Base S → 0 ˙ + S i = i
22 12 oveqd ⊢ R ∈ Ring ∧ i ∈ Base S → i LSSum ⁡ R 0 ˙ = i + S 0 ˙
23 2 10 lsm01 ⊢ i ∈ SubGrp ⁡ R → i LSSum ⁡ R 0 ˙ = i
24 18 23 syl ⊢ R ∈ Ring ∧ i ∈ Base S → i LSSum ⁡ R 0 ˙ = i
25 22 24 eqtr3d ⊢ R ∈ Ring ∧ i ∈ Base S → i + S 0 ˙ = i
26 3 4 5 9 21 25 ismgmid2 ⊢ R ∈ Ring → 0 ˙ = 0 S