Step |
Hyp |
Ref |
Expression |
1 |
|
mulcmpblnrlem |
|- ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( D .P. F ) +P. ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) ) = ( ( D .P. F ) +P. ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) ) ) |
2 |
|
mulclpr |
|- ( ( D e. P. /\ F e. P. ) -> ( D .P. F ) e. P. ) |
3 |
2
|
ad2ant2lr |
|- ( ( ( C e. P. /\ D e. P. ) /\ ( F e. P. /\ G e. P. ) ) -> ( D .P. F ) e. P. ) |
4 |
3
|
ad2ant2lr |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( D .P. F ) e. P. ) |
5 |
|
simplll |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> A e. P. ) |
6 |
|
simprll |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> F e. P. ) |
7 |
|
mulclpr |
|- ( ( A e. P. /\ F e. P. ) -> ( A .P. F ) e. P. ) |
8 |
5 6 7
|
syl2anc |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( A .P. F ) e. P. ) |
9 |
|
simpllr |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> B e. P. ) |
10 |
|
simprlr |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> G e. P. ) |
11 |
|
mulclpr |
|- ( ( B e. P. /\ G e. P. ) -> ( B .P. G ) e. P. ) |
12 |
9 10 11
|
syl2anc |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( B .P. G ) e. P. ) |
13 |
|
addclpr |
|- ( ( ( A .P. F ) e. P. /\ ( B .P. G ) e. P. ) -> ( ( A .P. F ) +P. ( B .P. G ) ) e. P. ) |
14 |
8 12 13
|
syl2anc |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( A .P. F ) +P. ( B .P. G ) ) e. P. ) |
15 |
|
simplrl |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> C e. P. ) |
16 |
|
simprrr |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> S e. P. ) |
17 |
|
mulclpr |
|- ( ( C e. P. /\ S e. P. ) -> ( C .P. S ) e. P. ) |
18 |
15 16 17
|
syl2anc |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( C .P. S ) e. P. ) |
19 |
|
simplrr |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> D e. P. ) |
20 |
|
simprrl |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> R e. P. ) |
21 |
|
mulclpr |
|- ( ( D e. P. /\ R e. P. ) -> ( D .P. R ) e. P. ) |
22 |
19 20 21
|
syl2anc |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( D .P. R ) e. P. ) |
23 |
|
addclpr |
|- ( ( ( C .P. S ) e. P. /\ ( D .P. R ) e. P. ) -> ( ( C .P. S ) +P. ( D .P. R ) ) e. P. ) |
24 |
18 22 23
|
syl2anc |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( C .P. S ) +P. ( D .P. R ) ) e. P. ) |
25 |
|
addclpr |
|- ( ( ( ( A .P. F ) +P. ( B .P. G ) ) e. P. /\ ( ( C .P. S ) +P. ( D .P. R ) ) e. P. ) -> ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) e. P. ) |
26 |
14 24 25
|
syl2anc |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) e. P. ) |
27 |
|
addcanpr |
|- ( ( ( D .P. F ) e. P. /\ ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) e. P. ) -> ( ( ( D .P. F ) +P. ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) ) = ( ( D .P. F ) +P. ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) ) -> ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) = ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) ) ) |
28 |
4 26 27
|
syl2anc |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( D .P. F ) +P. ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) ) = ( ( D .P. F ) +P. ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) ) -> ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) = ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) ) ) |
29 |
1 28
|
syl5 |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) = ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) ) ) |
30 |
|
mulclpr |
|- ( ( A e. P. /\ G e. P. ) -> ( A .P. G ) e. P. ) |
31 |
|
mulclpr |
|- ( ( B e. P. /\ F e. P. ) -> ( B .P. F ) e. P. ) |
32 |
|
addclpr |
|- ( ( ( A .P. G ) e. P. /\ ( B .P. F ) e. P. ) -> ( ( A .P. G ) +P. ( B .P. F ) ) e. P. ) |
33 |
30 31 32
|
syl2an |
|- ( ( ( A e. P. /\ G e. P. ) /\ ( B e. P. /\ F e. P. ) ) -> ( ( A .P. G ) +P. ( B .P. F ) ) e. P. ) |
34 |
5 10 9 6 33
|
syl22anc |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( A .P. G ) +P. ( B .P. F ) ) e. P. ) |
35 |
|
mulclpr |
|- ( ( C e. P. /\ R e. P. ) -> ( C .P. R ) e. P. ) |
36 |
|
mulclpr |
|- ( ( D e. P. /\ S e. P. ) -> ( D .P. S ) e. P. ) |
37 |
|
addclpr |
|- ( ( ( C .P. R ) e. P. /\ ( D .P. S ) e. P. ) -> ( ( C .P. R ) +P. ( D .P. S ) ) e. P. ) |
38 |
35 36 37
|
syl2an |
|- ( ( ( C e. P. /\ R e. P. ) /\ ( D e. P. /\ S e. P. ) ) -> ( ( C .P. R ) +P. ( D .P. S ) ) e. P. ) |
39 |
15 20 19 16 38
|
syl22anc |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( C .P. R ) +P. ( D .P. S ) ) e. P. ) |
40 |
|
enrbreq |
|- ( ( ( ( ( A .P. F ) +P. ( B .P. G ) ) e. P. /\ ( ( A .P. G ) +P. ( B .P. F ) ) e. P. ) /\ ( ( ( C .P. R ) +P. ( D .P. S ) ) e. P. /\ ( ( C .P. S ) +P. ( D .P. R ) ) e. P. ) ) -> ( <. ( ( A .P. F ) +P. ( B .P. G ) ) , ( ( A .P. G ) +P. ( B .P. F ) ) >. ~R <. ( ( C .P. R ) +P. ( D .P. S ) ) , ( ( C .P. S ) +P. ( D .P. R ) ) >. <-> ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) = ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) ) ) |
41 |
14 34 39 24 40
|
syl22anc |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( <. ( ( A .P. F ) +P. ( B .P. G ) ) , ( ( A .P. G ) +P. ( B .P. F ) ) >. ~R <. ( ( C .P. R ) +P. ( D .P. S ) ) , ( ( C .P. S ) +P. ( D .P. R ) ) >. <-> ( ( ( A .P. F ) +P. ( B .P. G ) ) +P. ( ( C .P. S ) +P. ( D .P. R ) ) ) = ( ( ( A .P. G ) +P. ( B .P. F ) ) +P. ( ( C .P. R ) +P. ( D .P. S ) ) ) ) ) |
42 |
29 41
|
sylibrd |
|- ( ( ( ( A e. P. /\ B e. P. ) /\ ( C e. P. /\ D e. P. ) ) /\ ( ( F e. P. /\ G e. P. ) /\ ( R e. P. /\ S e. P. ) ) ) -> ( ( ( A +P. D ) = ( B +P. C ) /\ ( F +P. S ) = ( G +P. R ) ) -> <. ( ( A .P. F ) +P. ( B .P. G ) ) , ( ( A .P. G ) +P. ( B .P. F ) ) >. ~R <. ( ( C .P. R ) +P. ( D .P. S ) ) , ( ( C .P. S ) +P. ( D .P. R ) ) >. ) ) |