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. ) |