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	⊢ 𝑆 = ( IDLsrg ‘ 𝑅 )
	idlsrg0g.2	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	idlsrg0g	⊢ ( 𝑅 ∈ Ring → { 0 } = ( 0g ‘ 𝑆 ) )

Proof

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