Metamath Proof Explorer

Theorem 1idsr

Description: 1 is an identity element for multiplication. (Contributed by NM, 2-May-1996) (New usage is discouraged.)

Ref Expression
Assertion 1idsr 
|- ( A e. R. -> ( A .R 1R ) = A )

Proof

Step Hyp Ref Expression
1 df-nr 
 |-  R. = ( ( P. X. P. ) /. ~R )
2 oveq1 
 |-  ( [ <. x , y >. ] ~R = A -> ( [ <. x , y >. ] ~R .R 1R ) = ( A .R 1R ) )
3 id 
 |-  ( [ <. x , y >. ] ~R = A -> [ <. x , y >. ] ~R = A )
4 2 3 eqeq12d 
 |-  ( [ <. x , y >. ] ~R = A -> ( ( [ <. x , y >. ] ~R .R 1R ) = [ <. x , y >. ] ~R <-> ( A .R 1R ) = A ) )
5 df-1r 
 |-  1R = [ <. ( 1P +P. 1P ) , 1P >. ] ~R
6 5 oveq2i 
 |-  ( [ <. x , y >. ] ~R .R 1R ) = ( [ <. x , y >. ] ~R .R [ <. ( 1P +P. 1P ) , 1P >. ] ~R )
7 1pr 
 |-  1P e. P.
8 addclpr 
 |-  ( ( 1P e. P. /\ 1P e. P. ) -> ( 1P +P. 1P ) e. P. )
9 7 7 8 mp2an 
 |-  ( 1P +P. 1P ) e. P.
10 mulsrpr 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( ( 1P +P. 1P ) e. P. /\ 1P e. P. ) ) -> ( [ <. x , y >. ] ~R .R [ <. ( 1P +P. 1P ) , 1P >. ] ~R ) = [ <. ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) >. ] ~R )
11 9 7 10 mpanr12 
 |-  ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R .R [ <. ( 1P +P. 1P ) , 1P >. ] ~R ) = [ <. ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) >. ] ~R )
12 distrpr 
 |-  ( x .P. ( 1P +P. 1P ) ) = ( ( x .P. 1P ) +P. ( x .P. 1P ) )
13 1idpr 
 |-  ( x e. P. -> ( x .P. 1P ) = x )
14 13 oveq1d 
 |-  ( x e. P. -> ( ( x .P. 1P ) +P. ( x .P. 1P ) ) = ( x +P. ( x .P. 1P ) ) )
15 12 14 syl5req 
 |-  ( x e. P. -> ( x +P. ( x .P. 1P ) ) = ( x .P. ( 1P +P. 1P ) ) )
16 distrpr 
 |-  ( y .P. ( 1P +P. 1P ) ) = ( ( y .P. 1P ) +P. ( y .P. 1P ) )
17 1idpr 
 |-  ( y e. P. -> ( y .P. 1P ) = y )
18 17 oveq1d 
 |-  ( y e. P. -> ( ( y .P. 1P ) +P. ( y .P. 1P ) ) = ( y +P. ( y .P. 1P ) ) )
19 16 18 syl5eq 
 |-  ( y e. P. -> ( y .P. ( 1P +P. 1P ) ) = ( y +P. ( y .P. 1P ) ) )
20 15 19 oveqan12d 
 |-  ( ( x e. P. /\ y e. P. ) -> ( ( x +P. ( x .P. 1P ) ) +P. ( y .P. ( 1P +P. 1P ) ) ) = ( ( x .P. ( 1P +P. 1P ) ) +P. ( y +P. ( y .P. 1P ) ) ) )
21 addasspr 
 |-  ( ( x +P. ( x .P. 1P ) ) +P. ( y .P. ( 1P +P. 1P ) ) ) = ( x +P. ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) )
22 ovex 
 |-  ( x .P. ( 1P +P. 1P ) ) e. _V
23 vex 
 |-  y e. _V
24 ovex 
 |-  ( y .P. 1P ) e. _V
25 addcompr 
 |-  ( z +P. w ) = ( w +P. z )
26 addasspr 
 |-  ( ( z +P. w ) +P. v ) = ( z +P. ( w +P. v ) )
27 22 23 24 25 26 caov12 
 |-  ( ( x .P. ( 1P +P. 1P ) ) +P. ( y +P. ( y .P. 1P ) ) ) = ( y +P. ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) )
28 20 21 27 3eqtr3g 
 |-  ( ( x e. P. /\ y e. P. ) -> ( x +P. ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) ) = ( y +P. ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) ) )
29 mulclpr 
 |-  ( ( x e. P. /\ ( 1P +P. 1P ) e. P. ) -> ( x .P. ( 1P +P. 1P ) ) e. P. )
30 9 29 mpan2 
 |-  ( x e. P. -> ( x .P. ( 1P +P. 1P ) ) e. P. )
31 mulclpr 
 |-  ( ( y e. P. /\ 1P e. P. ) -> ( y .P. 1P ) e. P. )
32 7 31 mpan2 
 |-  ( y e. P. -> ( y .P. 1P ) e. P. )
33 addclpr 
 |-  ( ( ( x .P. ( 1P +P. 1P ) ) e. P. /\ ( y .P. 1P ) e. P. ) -> ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) e. P. )
34 30 32 33 syl2an 
 |-  ( ( x e. P. /\ y e. P. ) -> ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) e. P. )
35 mulclpr 
 |-  ( ( x e. P. /\ 1P e. P. ) -> ( x .P. 1P ) e. P. )
36 7 35 mpan2 
 |-  ( x e. P. -> ( x .P. 1P ) e. P. )
37 mulclpr 
 |-  ( ( y e. P. /\ ( 1P +P. 1P ) e. P. ) -> ( y .P. ( 1P +P. 1P ) ) e. P. )
38 9 37 mpan2 
 |-  ( y e. P. -> ( y .P. ( 1P +P. 1P ) ) e. P. )
39 addclpr 
 |-  ( ( ( x .P. 1P ) e. P. /\ ( y .P. ( 1P +P. 1P ) ) e. P. ) -> ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) e. P. )
40 36 38 39 syl2an 
 |-  ( ( x e. P. /\ y e. P. ) -> ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) e. P. )
41 34 40 anim12i 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( x e. P. /\ y e. P. ) ) -> ( ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) e. P. /\ ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) e. P. ) )
42 enreceq 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) e. P. /\ ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) e. P. ) ) -> ( [ <. x , y >. ] ~R = [ <. ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) >. ] ~R <-> ( x +P. ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) ) = ( y +P. ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) ) ) )
43 41 42 syldan 
 |-  ( ( ( x e. P. /\ y e. P. ) /\ ( x e. P. /\ y e. P. ) ) -> ( [ <. x , y >. ] ~R = [ <. ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) >. ] ~R <-> ( x +P. ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) ) = ( y +P. ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) ) ) )
44 43 anidms 
 |-  ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R = [ <. ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) >. ] ~R <-> ( x +P. ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) ) = ( y +P. ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) ) ) )
45 28 44 mpbird 
 |-  ( ( x e. P. /\ y e. P. ) -> [ <. x , y >. ] ~R = [ <. ( ( x .P. ( 1P +P. 1P ) ) +P. ( y .P. 1P ) ) , ( ( x .P. 1P ) +P. ( y .P. ( 1P +P. 1P ) ) ) >. ] ~R )
46 11 45 eqtr4d 
 |-  ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R .R [ <. ( 1P +P. 1P ) , 1P >. ] ~R ) = [ <. x , y >. ] ~R )
47 6 46 syl5eq 
 |-  ( ( x e. P. /\ y e. P. ) -> ( [ <. x , y >. ] ~R .R 1R ) = [ <. x , y >. ] ~R )
48 1 4 47 ecoptocl 
 |-  ( A e. R. -> ( A .R 1R ) = A )