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
|
eqtr2id |
|- ( 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
|
eqtrid |
|- ( 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
|
eqtrid |
|- ( ( 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 ) |