This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )