Metamath Proof Explorer


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 )