Metamath Proof Explorer

Theorem mulcmpblnr

Description: Lemma showing compatibility of multiplication. (Contributed by NM, 5-Sep-1995) (New usage is discouraged.)

Ref Expression
Assertion mulcmpblnr 
|- ( ( ( ( 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 ) ) >. ) )

Proof

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