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 syl5eq 
 |-  ( 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 ) ) )