Metamath Proof Explorer


Theorem distrlem4pr

Description: Lemma for distributive law for positive reals. (Contributed by NM, 2-May-1996) (Revised by Mario Carneiro, 14-Jun-2013) (New usage is discouraged.)

Ref Expression
Assertion distrlem4pr
|- ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) )

Proof

Step Hyp Ref Expression
1 simpl2
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> B e. P. )
2 simprlr
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> y e. B )
3 elprnq
 |-  ( ( B e. P. /\ y e. B ) -> y e. Q. )
4 1 2 3 syl2anc
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> y e. Q. )
5 simp1
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> A e. P. )
6 simprl
 |-  ( ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) -> f e. A )
7 elprnq
 |-  ( ( A e. P. /\ f e. A ) -> f e. Q. )
8 5 6 7 syl2an
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> f e. Q. )
9 simpl3
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> C e. P. )
10 simprrr
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> z e. C )
11 elprnq
 |-  ( ( C e. P. /\ z e. C ) -> z e. Q. )
12 9 10 11 syl2anc
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> z e. Q. )
13 vex
 |-  x e. _V
14 vex
 |-  f e. _V
15 ltmnq
 |-  ( u e. Q. -> ( w  ( u .Q w ) 
16 vex
 |-  y e. _V
17 mulcomnq
 |-  ( w .Q v ) = ( v .Q w )
18 13 14 15 16 17 caovord2
 |-  ( y e. Q. -> ( x  ( x .Q y ) 
19 mulclnq
 |-  ( ( f e. Q. /\ z e. Q. ) -> ( f .Q z ) e. Q. )
20 ovex
 |-  ( x .Q y ) e. _V
21 ovex
 |-  ( f .Q y ) e. _V
22 ltanq
 |-  ( u e. Q. -> ( w  ( u +Q w ) 
23 ovex
 |-  ( f .Q z ) e. _V
24 addcomnq
 |-  ( w +Q v ) = ( v +Q w )
25 20 21 22 23 24 caovord2
 |-  ( ( f .Q z ) e. Q. -> ( ( x .Q y )  ( ( x .Q y ) +Q ( f .Q z ) ) 
26 19 25 syl
 |-  ( ( f e. Q. /\ z e. Q. ) -> ( ( x .Q y )  ( ( x .Q y ) +Q ( f .Q z ) ) 
27 18 26 sylan9bb
 |-  ( ( y e. Q. /\ ( f e. Q. /\ z e. Q. ) ) -> ( x  ( ( x .Q y ) +Q ( f .Q z ) ) 
28 4 8 12 27 syl12anc
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( x  ( ( x .Q y ) +Q ( f .Q z ) ) 
29 simpl1
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> A e. P. )
30 addclpr
 |-  ( ( B e. P. /\ C e. P. ) -> ( B +P. C ) e. P. )
31 30 3adant1
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( B +P. C ) e. P. )
32 31 adantr
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( B +P. C ) e. P. )
33 mulclpr
 |-  ( ( A e. P. /\ ( B +P. C ) e. P. ) -> ( A .P. ( B +P. C ) ) e. P. )
34 29 32 33 syl2anc
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( A .P. ( B +P. C ) ) e. P. )
35 distrnq
 |-  ( f .Q ( y +Q z ) ) = ( ( f .Q y ) +Q ( f .Q z ) )
36 simprrl
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> f e. A )
37 df-plp
 |-  +P. = ( u e. P. , v e. P. |-> { w | E. g e. u E. h e. v w = ( g +Q h ) } )
38 addclnq
 |-  ( ( g e. Q. /\ h e. Q. ) -> ( g +Q h ) e. Q. )
39 37 38 genpprecl
 |-  ( ( B e. P. /\ C e. P. ) -> ( ( y e. B /\ z e. C ) -> ( y +Q z ) e. ( B +P. C ) ) )
40 39 imp
 |-  ( ( ( B e. P. /\ C e. P. ) /\ ( y e. B /\ z e. C ) ) -> ( y +Q z ) e. ( B +P. C ) )
41 1 9 2 10 40 syl22anc
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( y +Q z ) e. ( B +P. C ) )
42 df-mp
 |-  .P. = ( u e. P. , v e. P. |-> { w | E. g e. u E. h e. v w = ( g .Q h ) } )
43 mulclnq
 |-  ( ( g e. Q. /\ h e. Q. ) -> ( g .Q h ) e. Q. )
44 42 43 genpprecl
 |-  ( ( A e. P. /\ ( B +P. C ) e. P. ) -> ( ( f e. A /\ ( y +Q z ) e. ( B +P. C ) ) -> ( f .Q ( y +Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
45 44 imp
 |-  ( ( ( A e. P. /\ ( B +P. C ) e. P. ) /\ ( f e. A /\ ( y +Q z ) e. ( B +P. C ) ) ) -> ( f .Q ( y +Q z ) ) e. ( A .P. ( B +P. C ) ) )
46 29 32 36 41 45 syl22anc
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( f .Q ( y +Q z ) ) e. ( A .P. ( B +P. C ) ) )
47 35 46 eqeltrrid
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( ( f .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) )
48 prcdnq
 |-  ( ( ( A .P. ( B +P. C ) ) e. P. /\ ( ( f .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) -> ( ( ( x .Q y ) +Q ( f .Q z ) )  ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
49 34 47 48 syl2anc
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( ( ( x .Q y ) +Q ( f .Q z ) )  ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
50 28 49 sylbid
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( x  ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
51 simpll
 |-  ( ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) -> x e. A )
52 elprnq
 |-  ( ( A e. P. /\ x e. A ) -> x e. Q. )
53 5 51 52 syl2an
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> x e. Q. )
54 vex
 |-  z e. _V
55 14 13 15 54 17 caovord2
 |-  ( z e. Q. -> ( f  ( f .Q z ) 
56 mulclnq
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( x .Q y ) e. Q. )
57 ltanq
 |-  ( ( x .Q y ) e. Q. -> ( ( f .Q z )  ( ( x .Q y ) +Q ( f .Q z ) ) 
58 56 57 syl
 |-  ( ( x e. Q. /\ y e. Q. ) -> ( ( f .Q z )  ( ( x .Q y ) +Q ( f .Q z ) ) 
59 55 58 sylan9bbr
 |-  ( ( ( x e. Q. /\ y e. Q. ) /\ z e. Q. ) -> ( f  ( ( x .Q y ) +Q ( f .Q z ) ) 
60 53 4 12 59 syl21anc
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( f  ( ( x .Q y ) +Q ( f .Q z ) ) 
61 distrnq
 |-  ( x .Q ( y +Q z ) ) = ( ( x .Q y ) +Q ( x .Q z ) )
62 simprll
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> x e. A )
63 42 43 genpprecl
 |-  ( ( A e. P. /\ ( B +P. C ) e. P. ) -> ( ( x e. A /\ ( y +Q z ) e. ( B +P. C ) ) -> ( x .Q ( y +Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
64 63 imp
 |-  ( ( ( A e. P. /\ ( B +P. C ) e. P. ) /\ ( x e. A /\ ( y +Q z ) e. ( B +P. C ) ) ) -> ( x .Q ( y +Q z ) ) e. ( A .P. ( B +P. C ) ) )
65 29 32 62 41 64 syl22anc
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( x .Q ( y +Q z ) ) e. ( A .P. ( B +P. C ) ) )
66 61 65 eqeltrrid
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( ( x .Q y ) +Q ( x .Q z ) ) e. ( A .P. ( B +P. C ) ) )
67 prcdnq
 |-  ( ( ( A .P. ( B +P. C ) ) e. P. /\ ( ( x .Q y ) +Q ( x .Q z ) ) e. ( A .P. ( B +P. C ) ) ) -> ( ( ( x .Q y ) +Q ( f .Q z ) )  ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
68 34 66 67 syl2anc
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( ( ( x .Q y ) +Q ( f .Q z ) )  ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
69 60 68 sylbid
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( f  ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
70 ltsonq
 |-  
71 sotrieq
 |-  ( (  ( x = f <-> -. ( x 
72 70 71 mpan
 |-  ( ( x e. Q. /\ f e. Q. ) -> ( x = f <-> -. ( x 
73 53 8 72 syl2anc
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( x = f <-> -. ( x 
74 oveq1
 |-  ( x = f -> ( x .Q z ) = ( f .Q z ) )
75 74 oveq2d
 |-  ( x = f -> ( ( x .Q y ) +Q ( x .Q z ) ) = ( ( x .Q y ) +Q ( f .Q z ) ) )
76 61 75 eqtrid
 |-  ( x = f -> ( x .Q ( y +Q z ) ) = ( ( x .Q y ) +Q ( f .Q z ) ) )
77 76 eleq1d
 |-  ( x = f -> ( ( x .Q ( y +Q z ) ) e. ( A .P. ( B +P. C ) ) <-> ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
78 65 77 syl5ibcom
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( x = f -> ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
79 73 78 sylbird
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( -. ( x  ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
80 50 69 79 ecase3d
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) )