Metamath Proof Explorer

Theorem distrlem5pr

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 distrlem5pr 
|- ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A .P. B ) +P. ( A .P. C ) ) C_ ( A .P. ( B +P. C ) ) )

Proof

Step Hyp Ref Expression
1 mulclpr 
 |-  ( ( A e. P. /\ B e. P. ) -> ( A .P. B ) e. P. )
2 1 3adant3 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( A .P. B ) e. P. )
3 mulclpr 
 |-  ( ( A e. P. /\ C e. P. ) -> ( A .P. C ) e. P. )
4 df-plp 
 |-  +P. = ( x e. P. , y e. P. |-> { f | E. g e. x E. h e. y f = ( g +Q h ) } )
5 addclnq 
 |-  ( ( g e. Q. /\ h e. Q. ) -> ( g +Q h ) e. Q. )
6 4 5 genpelv 
 |-  ( ( ( A .P. B ) e. P. /\ ( A .P. C ) e. P. ) -> ( w e. ( ( A .P. B ) +P. ( A .P. C ) ) <-> E. v e. ( A .P. B ) E. u e. ( A .P. C ) w = ( v +Q u ) ) )
7 2 3 6 3imp3i2an 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( w e. ( ( A .P. B ) +P. ( A .P. C ) ) <-> E. v e. ( A .P. B ) E. u e. ( A .P. C ) w = ( v +Q u ) ) )
8 df-mp 
 |-  .P. = ( w e. P. , v e. P. |-> { x | E. g e. w E. h e. v x = ( g .Q h ) } )
9 mulclnq 
 |-  ( ( g e. Q. /\ h e. Q. ) -> ( g .Q h ) e. Q. )
10 8 9 genpelv 
 |-  ( ( A e. P. /\ C e. P. ) -> ( u e. ( A .P. C ) <-> E. f e. A E. z e. C u = ( f .Q z ) ) )
11 10 3adant2 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( u e. ( A .P. C ) <-> E. f e. A E. z e. C u = ( f .Q z ) ) )
12 11 anbi2d 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( v e. ( A .P. B ) /\ u e. ( A .P. C ) ) <-> ( v e. ( A .P. B ) /\ E. f e. A E. z e. C u = ( f .Q z ) ) ) )
13 df-mp 
 |-  .P. = ( w e. P. , v e. P. |-> { f | E. g e. w E. h e. v f = ( g .Q h ) } )
14 13 9 genpelv 
 |-  ( ( A e. P. /\ B e. P. ) -> ( v e. ( A .P. B ) <-> E. x e. A E. y e. B v = ( x .Q y ) ) )
15 14 3adant3 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( v e. ( A .P. B ) <-> E. x e. A E. y e. B v = ( x .Q y ) ) )
16 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 ) ) )
17 oveq12 
 |-  ( ( v = ( x .Q y ) /\ u = ( f .Q z ) ) -> ( v +Q u ) = ( ( x .Q y ) +Q ( f .Q z ) ) )
18 17 eqeq2d 
 |-  ( ( v = ( x .Q y ) /\ u = ( f .Q z ) ) -> ( w = ( v +Q u ) <-> w = ( ( x .Q y ) +Q ( f .Q z ) ) ) )
19 eleq1 
 |-  ( w = ( ( x .Q y ) +Q ( f .Q z ) ) -> ( w e. ( A .P. ( B +P. C ) ) <-> ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
20 18 19 biimtrdi 
 |-  ( ( v = ( x .Q y ) /\ u = ( f .Q z ) ) -> ( w = ( v +Q u ) -> ( w e. ( A .P. ( B +P. C ) ) <-> ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) ) )
21 20 imp 
 |-  ( ( ( v = ( x .Q y ) /\ u = ( f .Q z ) ) /\ w = ( v +Q u ) ) -> ( w e. ( A .P. ( B +P. C ) ) <-> ( ( x .Q y ) +Q ( f .Q z ) ) e. ( A .P. ( B +P. C ) ) ) )
22 16 21 syl5ibrcom 
 |-  ( ( ( A e. P. /\ B e. P. /\ C e. P. ) /\ ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) ) -> ( ( ( v = ( x .Q y ) /\ u = ( f .Q z ) ) /\ w = ( v +Q u ) ) -> w e. ( A .P. ( B +P. C ) ) ) )
23 22 exp4b 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) -> ( ( v = ( x .Q y ) /\ u = ( f .Q z ) ) -> ( w = ( v +Q u ) -> w e. ( A .P. ( B +P. C ) ) ) ) ) )
24 23 com3l 
 |-  ( ( ( x e. A /\ y e. B ) /\ ( f e. A /\ z e. C ) ) -> ( ( v = ( x .Q y ) /\ u = ( f .Q z ) ) -> ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( w = ( v +Q u ) -> w e. ( A .P. ( B +P. C ) ) ) ) ) )
25 24 exp4b 
 |-  ( ( x e. A /\ y e. B ) -> ( ( f e. A /\ z e. C ) -> ( v = ( x .Q y ) -> ( u = ( f .Q z ) -> ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( w = ( v +Q u ) -> w e. ( A .P. ( B +P. C ) ) ) ) ) ) ) )
26 25 com23 
 |-  ( ( x e. A /\ y e. B ) -> ( v = ( x .Q y ) -> ( ( f e. A /\ z e. C ) -> ( u = ( f .Q z ) -> ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( w = ( v +Q u ) -> w e. ( A .P. ( B +P. C ) ) ) ) ) ) ) )
27 26 rexlimivv 
 |-  ( E. x e. A E. y e. B v = ( x .Q y ) -> ( ( f e. A /\ z e. C ) -> ( u = ( f .Q z ) -> ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( w = ( v +Q u ) -> w e. ( A .P. ( B +P. C ) ) ) ) ) ) )
28 27 rexlimdvv 
 |-  ( E. x e. A E. y e. B v = ( x .Q y ) -> ( E. f e. A E. z e. C u = ( f .Q z ) -> ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( w = ( v +Q u ) -> w e. ( A .P. ( B +P. C ) ) ) ) ) )
29 28 com3r 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( E. x e. A E. y e. B v = ( x .Q y ) -> ( E. f e. A E. z e. C u = ( f .Q z ) -> ( w = ( v +Q u ) -> w e. ( A .P. ( B +P. C ) ) ) ) ) )
30 15 29 sylbid 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( v e. ( A .P. B ) -> ( E. f e. A E. z e. C u = ( f .Q z ) -> ( w = ( v +Q u ) -> w e. ( A .P. ( B +P. C ) ) ) ) ) )
31 30 impd 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( v e. ( A .P. B ) /\ E. f e. A E. z e. C u = ( f .Q z ) ) -> ( w = ( v +Q u ) -> w e. ( A .P. ( B +P. C ) ) ) ) )
32 12 31 sylbid 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( v e. ( A .P. B ) /\ u e. ( A .P. C ) ) -> ( w = ( v +Q u ) -> w e. ( A .P. ( B +P. C ) ) ) ) )
33 32 rexlimdvv 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( E. v e. ( A .P. B ) E. u e. ( A .P. C ) w = ( v +Q u ) -> w e. ( A .P. ( B +P. C ) ) ) )
34 7 33 sylbid 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( w e. ( ( A .P. B ) +P. ( A .P. C ) ) -> w e. ( A .P. ( B +P. C ) ) ) )
35 34 ssrdv 
 |-  ( ( A e. P. /\ B e. P. /\ C e. P. ) -> ( ( A .P. B ) +P. ( A .P. C ) ) C_ ( A .P. ( B +P. C ) ) )