Step |
Hyp |
Ref |
Expression |
1 |
|
df-nr |
|- R. = ( ( P. X. P. ) /. ~R ) |
2 |
|
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 ) |
3 |
|
mulsrpr |
|- ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( [ <. z , w >. ] ~R .R [ <. v , u >. ] ~R ) = [ <. ( ( z .P. v ) +P. ( w .P. u ) ) , ( ( z .P. u ) +P. ( w .P. v ) ) >. ] ~R ) |
4 |
|
mulsrpr |
|- ( ( ( ( ( x .P. z ) +P. ( y .P. w ) ) e. P. /\ ( ( x .P. w ) +P. ( y .P. z ) ) e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( [ <. ( ( x .P. z ) +P. ( y .P. w ) ) , ( ( x .P. w ) +P. ( y .P. z ) ) >. ] ~R .R [ <. v , u >. ] ~R ) = [ <. ( ( ( ( x .P. z ) +P. ( y .P. w ) ) .P. v ) +P. ( ( ( x .P. w ) +P. ( y .P. z ) ) .P. u ) ) , ( ( ( ( x .P. z ) +P. ( y .P. w ) ) .P. u ) +P. ( ( ( x .P. w ) +P. ( y .P. z ) ) .P. v ) ) >. ] ~R ) |
5 |
|
mulsrpr |
|- ( ( ( x e. P. /\ y e. P. ) /\ ( ( ( z .P. v ) +P. ( w .P. u ) ) e. P. /\ ( ( z .P. u ) +P. ( w .P. v ) ) e. P. ) ) -> ( [ <. x , y >. ] ~R .R [ <. ( ( z .P. v ) +P. ( w .P. u ) ) , ( ( z .P. u ) +P. ( w .P. v ) ) >. ] ~R ) = [ <. ( ( x .P. ( ( z .P. v ) +P. ( w .P. u ) ) ) +P. ( y .P. ( ( z .P. u ) +P. ( w .P. v ) ) ) ) , ( ( x .P. ( ( z .P. u ) +P. ( w .P. v ) ) ) +P. ( y .P. ( ( z .P. v ) +P. ( w .P. u ) ) ) ) >. ] ~R ) |
6 |
|
mulclpr |
|- ( ( x e. P. /\ z e. P. ) -> ( x .P. z ) e. P. ) |
7 |
|
mulclpr |
|- ( ( y e. P. /\ w e. P. ) -> ( y .P. w ) e. P. ) |
8 |
|
addclpr |
|- ( ( ( x .P. z ) e. P. /\ ( y .P. w ) e. P. ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) |
9 |
6 7 8
|
syl2an |
|- ( ( ( x e. P. /\ z e. P. ) /\ ( y e. P. /\ w e. P. ) ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) |
10 |
9
|
an4s |
|- ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x .P. z ) +P. ( y .P. w ) ) e. P. ) |
11 |
|
mulclpr |
|- ( ( x e. P. /\ w e. P. ) -> ( x .P. w ) e. P. ) |
12 |
|
mulclpr |
|- ( ( y e. P. /\ z e. P. ) -> ( y .P. z ) e. P. ) |
13 |
|
addclpr |
|- ( ( ( x .P. w ) e. P. /\ ( y .P. z ) e. P. ) -> ( ( x .P. w ) +P. ( y .P. z ) ) e. P. ) |
14 |
11 12 13
|
syl2an |
|- ( ( ( x e. P. /\ w e. P. ) /\ ( y e. P. /\ z e. P. ) ) -> ( ( x .P. w ) +P. ( y .P. z ) ) e. P. ) |
15 |
14
|
an42s |
|- ( ( ( x e. P. /\ y e. P. ) /\ ( z e. P. /\ w e. P. ) ) -> ( ( x .P. w ) +P. ( y .P. z ) ) e. P. ) |
16 |
10 15
|
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. ) ) |
17 |
|
mulclpr |
|- ( ( z e. P. /\ v e. P. ) -> ( z .P. v ) e. P. ) |
18 |
|
mulclpr |
|- ( ( w e. P. /\ u e. P. ) -> ( w .P. u ) e. P. ) |
19 |
|
addclpr |
|- ( ( ( z .P. v ) e. P. /\ ( w .P. u ) e. P. ) -> ( ( z .P. v ) +P. ( w .P. u ) ) e. P. ) |
20 |
17 18 19
|
syl2an |
|- ( ( ( z e. P. /\ v e. P. ) /\ ( w e. P. /\ u e. P. ) ) -> ( ( z .P. v ) +P. ( w .P. u ) ) e. P. ) |
21 |
20
|
an4s |
|- ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( z .P. v ) +P. ( w .P. u ) ) e. P. ) |
22 |
|
mulclpr |
|- ( ( z e. P. /\ u e. P. ) -> ( z .P. u ) e. P. ) |
23 |
|
mulclpr |
|- ( ( w e. P. /\ v e. P. ) -> ( w .P. v ) e. P. ) |
24 |
|
addclpr |
|- ( ( ( z .P. u ) e. P. /\ ( w .P. v ) e. P. ) -> ( ( z .P. u ) +P. ( w .P. v ) ) e. P. ) |
25 |
22 23 24
|
syl2an |
|- ( ( ( z e. P. /\ u e. P. ) /\ ( w e. P. /\ v e. P. ) ) -> ( ( z .P. u ) +P. ( w .P. v ) ) e. P. ) |
26 |
25
|
an42s |
|- ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( z .P. u ) +P. ( w .P. v ) ) e. P. ) |
27 |
21 26
|
jca |
|- ( ( ( z e. P. /\ w e. P. ) /\ ( v e. P. /\ u e. P. ) ) -> ( ( ( z .P. v ) +P. ( w .P. u ) ) e. P. /\ ( ( z .P. u ) +P. ( w .P. v ) ) e. P. ) ) |
28 |
|
vex |
|- x e. _V |
29 |
|
vex |
|- y e. _V |
30 |
|
vex |
|- z e. _V |
31 |
|
mulcompr |
|- ( f .P. g ) = ( g .P. f ) |
32 |
|
distrpr |
|- ( f .P. ( g +P. h ) ) = ( ( f .P. g ) +P. ( f .P. h ) ) |
33 |
|
vex |
|- w e. _V |
34 |
|
vex |
|- v e. _V |
35 |
|
mulasspr |
|- ( ( f .P. g ) .P. h ) = ( f .P. ( g .P. h ) ) |
36 |
|
vex |
|- u e. _V |
37 |
|
addcompr |
|- ( f +P. g ) = ( g +P. f ) |
38 |
|
addasspr |
|- ( ( f +P. g ) +P. h ) = ( f +P. ( g +P. h ) ) |
39 |
28 29 30 31 32 33 34 35 36 37 38
|
caovlem2 |
|- ( ( ( ( x .P. z ) +P. ( y .P. w ) ) .P. v ) +P. ( ( ( x .P. w ) +P. ( y .P. z ) ) .P. u ) ) = ( ( x .P. ( ( z .P. v ) +P. ( w .P. u ) ) ) +P. ( y .P. ( ( z .P. u ) +P. ( w .P. v ) ) ) ) |
40 |
28 29 30 31 32 33 36 35 34 37 38
|
caovlem2 |
|- ( ( ( ( x .P. z ) +P. ( y .P. w ) ) .P. u ) +P. ( ( ( x .P. w ) +P. ( y .P. z ) ) .P. v ) ) = ( ( x .P. ( ( z .P. u ) +P. ( w .P. v ) ) ) +P. ( y .P. ( ( z .P. v ) +P. ( w .P. u ) ) ) ) |
41 |
1 2 3 4 5 16 27 39 40
|
ecovass |
|- ( ( A e. R. /\ B e. R. /\ C e. R. ) -> ( ( A .R B ) .R C ) = ( A .R ( B .R C ) ) ) |
42 |
|
dmmulsr |
|- dom .R = ( R. X. R. ) |
43 |
|
0nsr |
|- -. (/) e. R. |
44 |
42 43
|
ndmovass |
|- ( -. ( A e. R. /\ B e. R. /\ C e. R. ) -> ( ( A .R B ) .R C ) = ( A .R ( B .R C ) ) ) |
45 |
41 44
|
pm2.61i |
|- ( ( A .R B ) .R C ) = ( A .R ( B .R C ) ) |