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	No typesetting found for \|- S = ( IDLsrg ` R ) with typecode \|-
	idlsrg0g.2	$⊢ \underset{˙}{0} = 0_{R}$
Assertion	idlsrg0g	$⊢ R \in Ring \to \{\underset{˙}{0}\} = 0_{S}$

Proof

Step	Hyp	Ref	Expression
1		idlsrg0g.1	Could not format S = ( IDLsrg ` R ) : No typesetting found for \|- S = ( IDLsrg ` R ) with typecode \|-
2		idlsrg0g.2	$⊢ \underset{˙}{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 \in Ring \to \{\underset{˙}{0}\} \in LIdeal (R)$
8	1 6	idlsrgbas	$⊢ R \in Ring \to LIdeal (R) = {Base}_{S}$
9	7 8	eleqtrd	$⊢ R \in Ring \to \{\underset{˙}{0}\} \in {Base}_{S}$
10		eqid	$⊢ LSSum (R) = LSSum (R)$
11	1 10	idlsrgplusg	$⊢ R \in Ring \to LSSum (R) = +_{S}$
12	11	adantr	$⊢ (R \in Ring \land i \in {Base}_{S}) \to LSSum (R) = +_{S}$
13	12	oveqd	$⊢ (R \in Ring \land i \in {Base}_{S}) \to \{\underset{˙}{0}\} LSSum (R) i = \{\underset{˙}{0}\} +_{S} i$
14		simpr	$⊢ (R \in Ring \land i \in {Base}_{S}) \to i \in {Base}_{S}$
15	8	adantr	$⊢ (R \in Ring \land i \in {Base}_{S}) \to LIdeal (R) = {Base}_{S}$
16	14 15	eleqtrrd	$⊢ (R \in Ring \land i \in {Base}_{S}) \to i \in LIdeal (R)$
17	6	lidlsubg	$⊢ (R \in Ring \land i \in LIdeal (R)) \to i \in SubGrp (R)$
18	16 17	syldan	$⊢ (R \in Ring \land i \in {Base}_{S}) \to i \in SubGrp (R)$
19	2 10	lsm02	$⊢ i \in SubGrp (R) \to \{\underset{˙}{0}\} LSSum (R) i = i$
20	18 19	syl	$⊢ (R \in Ring \land i \in {Base}_{S}) \to \{\underset{˙}{0}\} LSSum (R) i = i$
21	13 20	eqtr3d	$⊢ (R \in Ring \land i \in {Base}_{S}) \to \{\underset{˙}{0}\} +_{S} i = i$
22	12	oveqd	$⊢ (R \in Ring \land i \in {Base}_{S}) \to i LSSum (R) \{\underset{˙}{0}\} = i +_{S} \{\underset{˙}{0}\}$
23	2 10	lsm01	$⊢ i \in SubGrp (R) \to i LSSum (R) \{\underset{˙}{0}\} = i$
24	18 23	syl	$⊢ (R \in Ring \land i \in {Base}_{S}) \to i LSSum (R) \{\underset{˙}{0}\} = i$
25	22 24	eqtr3d	$⊢ (R \in Ring \land i \in {Base}_{S}) \to i +_{S} \{\underset{˙}{0}\} = i$
26	3 4 5 9 21 25	ismgmid2	$⊢ R \in Ring \to \{\underset{˙}{0}\} = 0_{S}$

Metamath Proof Explorer

Theorem idlsrg0g

Proof