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

Metamath Proof Explorer

Theorem addclsr

Description: Closure of addition on signed reals. (Contributed by NM, 25-Jul-1995) (New usage is discouraged.)

Ref Expression
Assertion addclsr 
|- ( ( A e. R. /\ B e. R. ) -> ( A +R B ) e. R. )

Proof

Step Hyp Ref Expression
1 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
2 oveq1 
 |-  ( [ <. x , y >. ] ~R = A -> ( [ <. x , y >. ] ~R +R [ <. z , w >. ] ~R ) = ( A +R [ <. z , w >. ] ~R ) )
3 2 eleq1d 
 |-  ( [ <. x , y >. ] ~R = A -> ( ( [ <. x , y >. ] ~R +R [ <. z , w >. ] ~R ) e. ( ( P. X. P. ) /. ~R ) <-> ( A +R [ <. z , w >. ] ~R ) e. ( ( P. X. P. ) /. ~R ) ) )
4 oveq2 
 |-  ( [ <. z , w >. ] ~R = B -> ( A +R [ <. z , w >. ] ~R ) = ( A +R B ) )
5 4 eleq1d 
 |-  ( [ <. z , w >. ] ~R = B -> ( ( A +R [ <. z , w >. ] ~R ) e. ( ( P. X. P. ) /. ~R ) <-> ( A +R B ) e. ( ( P. X. P. ) /. ~R ) ) )
6 addsrpr 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. x , y >. ] ~R +R [ <. z , w >. ] ~R ) = [ <. ( x +P. z ) , ( y +P. w ) >. ] ~R )
7 addclpr 
 |-  ( ( x e. P. /\ z e. P. ) -> ( x +P. z ) e. P. )
8 addclpr 
 |-  ( ( y e. P. /\ w e. P. ) -> ( y +P. w ) e. P. )
9 7 8 anim12i 
 |-  ( ( ( x e. P. /\ z e. P. ) /\ ( y e. P. /\ w e. P. ) ) -> ( ( x +P. z ) e. P. /\ ( y +P. w ) e. P. ) )
10 9 an4s 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x +P. z ) e. P. /\ ( y +P. w ) e. P. ) )
11 opelxpi 
 |-  ( ( ( x +P. z ) e. P. /\ ( y +P. w ) e. P. ) -> <. ( x +P. z ) , ( y +P. w ) >. e. ( P. X. P. ) )
12 enrex 
 |-  ~R e. _V
13 12 ecelqsi 
 |-  ( <. ( x +P. z ) , ( y +P. w ) >. e. ( P. X. P. ) -> [ <. ( x +P. z ) , ( y +P. w ) >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
14 10 11 13 3syl 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> [ <. ( x +P. z ) , ( y +P. w ) >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
15 6 14 eqeltrd 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. x , y >. ] ~R +R [ <. z , w >. ] ~R ) e. ( ( P. X. P. ) /. ~R ) )
16 1 3 5 15 2ecoptocl 
 |-  ( ( A e. R. /\ B e. R. ) -> ( A +R B ) e. ( ( P. X. P. ) /. ~R ) )
17 16 1 eleqtrrdi 
 |-  ( ( A e. R. /\ B e. R. ) -> ( A +R B ) e. R. )