Theorem lidlacl

Description: An ideal is closed under addition. (Contributed by Stefan O'Rear, 3-Jan-2015)

	Ref	Expression
Hypotheses	lidlcl.u	|- U = ( LIdeal ` R )
	lidlacl.p	|- .+ = ( +g ` R )
Assertion	lidlacl	|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. I /\ Y e. I ) ) -> ( X .+ Y ) e. I )

Proof

Step	Hyp	Ref	Expression
1		lidlcl.u	|- U = ( LIdeal ` R )
2		lidlacl.p	|- .+ = ( +g ` R )
3		rlmplusg	|- ( +g ` R ) = ( +g ` ( ringLMod ` R ) )
4	2 3	eqtri	|- .+ = ( +g ` ( ringLMod ` R ) )
5	4	oveqi	|- ( X .+ Y ) = ( X ( +g ` ( ringLMod ` R ) ) Y )
6		rlmlmod	|- ( R e. Ring -> ( ringLMod ` R ) e. LMod )
7	6	adantr	|- ( ( R e. Ring /\ I e. U ) -> ( ringLMod ` R ) e. LMod )
8		simpr	|- ( ( R e. Ring /\ I e. U ) -> I e. U )
9		lidlval	|- ( LIdeal ` R ) = ( LSubSp ` ( ringLMod ` R ) )
10	1 9	eqtri	|- U = ( LSubSp ` ( ringLMod ` R ) )
11	8 10	eleqtrdi	|- ( ( R e. Ring /\ I e. U ) -> I e. ( LSubSp ` ( ringLMod ` R ) ) )
12	7 11	jca	|- ( ( R e. Ring /\ I e. U ) -> ( ( ringLMod ` R ) e. LMod /\ I e. ( LSubSp ` ( ringLMod ` R ) ) ) )
13		eqid	|- ( +g ` ( ringLMod ` R ) ) = ( +g ` ( ringLMod ` R ) )
14		eqid	|- ( LSubSp ` ( ringLMod ` R ) ) = ( LSubSp ` ( ringLMod ` R ) )
15	13 14	lssvacl	|- ( ( ( ( ringLMod ` R ) e. LMod /\ I e. ( LSubSp ` ( ringLMod ` R ) ) ) /\ ( X e. I /\ Y e. I ) ) -> ( X ( +g ` ( ringLMod ` R ) ) Y ) e. I )
16	12 15	sylan	|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. I /\ Y e. I ) ) -> ( X ( +g ` ( ringLMod ` R ) ) Y ) e. I )
17	5 16	eqeltrid	|- ( ( ( R e. Ring /\ I e. U ) /\ ( X e. I /\ Y e. I ) ) -> ( X .+ Y ) e. I )