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

Metamath Proof Explorer

Theorem mulclsr

Description: Closure of multiplication on signed reals. (Contributed by NM, 10-Aug-1995) (New usage is discouraged.)

Ref Expression
Assertion mulclsr 
|- ( ( 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 mulsrpr 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( [ <. x , y >. ] ~R .R [ <. z , w >. ] ~R ) = [ <. ( ( x .P. z ) +P. ( y .P. w ) ) , ( ( x .P. w ) +P. ( y .P. z ) ) >. ] ~R )
7 mulclpr 
 |-  ( ( x e. P. /\ z e. P. ) -> ( x .P. z ) e. P. )
8 mulclpr 
 |-  ( ( y e. P. /\ w e. P. ) -> ( y .P. w ) e. P. )
9 addclpr 
 |-  ( ( ( x .P. z ) e. P. /\ ( y .P. w ) e. P. ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. )
10 7 8 9 syl2an 
 |-  ( ( ( x e. P. /\ z e. P. ) /\ ( y e. P. /\ w e. P. ) ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. )
11 10 an4s 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. )
12 mulclpr 
 |-  ( ( x e. P. /\ w e. P. ) -> ( x .P. w ) e. P. )
13 mulclpr 
 |-  ( ( y e. P. /\ z e. P. ) -> ( y .P. z ) e. P. )
14 addclpr 
 |-  ( ( ( x .P. w ) e. P. /\ ( y .P. z ) e. P. ) -> ( ( x .P. w ) +P. ( y .P. z ) ) e. P. )
15 12 13 14 syl2an 
 |-  ( ( ( x e. P. /\ w e. P. ) /\ ( y e. P. /\ z e. P. ) ) -> ( ( x .P. w ) +P. ( y .P. z ) ) e. P. )
16 15 an42s 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x .P. w ) +P. ( y .P. z ) ) e. P. )
17 11 16 jca 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( ( x .P. z ) +P. ( y .P. w ) ) e. P. /\ ( ( x .P. w ) +P. ( y .P. z ) ) e. P. ) )
18 opelxpi 
 |-  ( ( ( ( x .P. z ) +P. ( y .P. w ) ) e. P. /\ ( ( x .P. w ) +P. ( y .P. z ) ) e. P. ) -> <. ( ( x .P. z ) +P. ( y .P. w ) ) , ( ( x .P. w ) +P. ( y .P. z ) ) >. e. ( P. X. P. ) )
19 enrex 
 |-  ~R e. _V
20 19 ecelqsi 
 |-  ( <. ( ( x .P. z ) +P. ( y .P. w ) ) , ( ( x .P. w ) +P. ( y .P. z ) ) >. e. ( P. X. P. ) -> [ <. ( ( x .P. z ) +P. ( y .P. w ) ) , ( ( x .P. w ) +P. ( y .P. z ) ) >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
21 17 18 20 3syl 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> [ <. ( ( x .P. z ) +P. ( y .P. w ) ) , ( ( x .P. w ) +P. ( y .P. z ) ) >. ] ~R e. ( ( P. X. P. ) /. ~R ) )
22 6 21 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 ) )
23 1 3 5 22 2ecoptocl 
 |-  ( ( A e. R. /\ B e. R. ) -> ( A .R B ) e. ( ( P. X. P. ) /. ~R ) )
24 23 1 eleqtrrdi 
 |-  ( ( A e. R. /\ B e. R. ) -> ( A .R B ) e. R. )