HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem distrlem1pr 3921
Description: Lemma for distributive law for positive reals.
Assertion
Ref Expression
distrlem1pr |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (A .P (B +P. C)) (_ ((A .P B) +P. (A .P C)))
Proof of Theorem distrlem1pr
StepHypRef Expression
1 df-mp 3883 . . . . . . 7 |- .P = {<.<.y, z>., u>. | ((y e. P. /\ z e. P.) /\ u = {f | E.g e. y E.h e. z f = (g .Q h)})}
2 visset 1350 . . . . . . 7 |- w e. V
31, 2genpelv 3897 . . . . . 6 |- ((A e. P. /\ (B +P. C) e. P.) -> (w e. (A .P (B +P. C)) <-> E.xE.v((x e. A /\ v e. (B +P. C)) /\ w = (x .Q v))))
4 addclpr 3914 . . . . . 6 |- ((B e. P. /\ C e. P.) -> (B +P. C) e. P.)
53, 4sylan2 346 . . . . 5 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (w e. (A .P (B +P. C)) <-> E.xE.v((x e. A /\ v e. (B +P. C)) /\ w = (x .Q v))))
6 df-plp 3882 . . . . . . . . . . 11 |- +P. = {<.<.x, w>., u>. | ((x e. P. /\ w e. P.) /\ u = {f | E.g e. x E.h e. w f = (g +Q h)})}
7 visset 1350 . . . . . . . . . . 11 |- v e. V
86, 7genpelv 3897 . . . . . . . . . 10 |- ((B e. P. /\ C e. P.) -> (v e. (B +P. C) <-> E.yE.z((y e. B /\ z e. C) /\ v = (y +Q z))))
98anbi1d 469 . . . . . . . . 9 |- ((B e. P. /\ C e. P.) -> ((v e. (B +P. C) /\ w = (x .Q v)) <-> (E.yE.z((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))))
109anbi2d 468 . . . . . . . 8 |- ((B e. P. /\ C e. P.) -> ((x e. A /\ (v e. (B +P. C) /\ w = (x .Q v))) <-> (x e. A /\ (E.yE.z((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v)))))
11 anass 336 . . . . . . . 8 |- (((x e. A /\ v e. (B +P. C)) /\ w = (x .Q v)) <-> (x e. A /\ (v e. (B +P. C) /\ w = (x .Q v))))
12 19.42vv 968 . . . . . . . . 9 |- (E.yE.z(x e. A /\ (((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))) <-> (x e. A /\ E.yE.z(((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))))
13 19.41vv 964 . . . . . . . . . 10 |- (E.yE.z(((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v)) <-> (E.yE.z((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v)))
1413anbi2i 367 . . . . . . . . 9 |- ((x e. A /\ E.yE.z(((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))) <-> (x e. A /\ (E.yE.z((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))))
1512, 14bitr 151 . . . . . . . 8 |- (E.yE.z(x e. A /\ (((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))) <-> (x e. A /\ (E.yE.z((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))))
1610, 11, 153bitr4g 428 . . . . . . 7 |- ((B e. P. /\ C e. P.) -> (((x e. A /\ v e. (B +P. C)) /\ w = (x .Q v)) <-> E.yE.z(x e. A /\ (((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v)))))
1716adantl 305 . . . . . 6 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (((x e. A /\ v e. (B +P. C)) /\ w = (x .Q v)) <-> E.yE.z(x e. A /\ (((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v)))))
1817bi2exdv 938 . . . . 5 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (E.xE.v((x e. A /\ v e. (B +P. C)) /\ w = (x .Q v)) <-> E.xE.vE.yE.z(x e. A /\ (((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v)))))
195, 18bitrd 406 . . . 4 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (w e. (A .P (B +P. C)) <-> E.xE.vE.yE.z(x e. A /\ (((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v)))))
20 exrot4 778 . . . . 5 |- (E.xE.vE.yE.z(x e. A /\ (((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))) <-> E.yE.zE.xE.v(x e. A /\ (((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))))
21 anass 336 . . . . . . . . . 10 |- ((((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v)) <-> ((y e. B /\ z e. C) /\ (v = (y +Q z) /\ w = (x .Q v))))
2221biex 733 . . . . . . . . 9 |- (E.v(((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v)) <-> E.v((y e. B /\ z e. C) /\ (v = (y +Q z) /\ w = (x .Q v))))
23 19.42v 966 . . . . . . . . 9 |- (E.v((y e. B /\ z e. C) /\ (v = (y +Q z) /\ w = (x .Q v))) <-> ((y e. B /\ z e. C) /\ E.v(v = (y +Q z) /\ w = (x .Q v))))
24 oprex 3018 . . . . . . . . . . 11 |- (y +Q z) e. V
25 opreq2 3007 . . . . . . . . . . . 12 |- (v = (y +Q z) -> (x .Q v) = (x .Q (y +Q z)))
2625cleq2d 1112 . . . . . . . . . . 11 |- (v = (y +Q z) -> (w = (x .Q v) <-> w = (x .Q (y +Q z))))
2724, 26ceqsexv 1371 . . . . . . . . . 10 |- (E.v(v = (y +Q z) /\ w = (x .Q v)) <-> w = (x .Q (y +Q z)))
2827anbi2i 367 . . . . . . . . 9 |- (((y e. B /\ z e. C) /\ E.v(v = (y +Q z) /\ w = (x .Q v))) <-> ((y e. B /\ z e. C) /\ w = (x .Q (y +Q z))))
2922, 23, 283bitr 155 . . . . . . . 8 |- (E.v(((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v)) <-> ((y e. B /\ z e. C) /\ w = (x .Q (y +Q z))))
3029anbi2i 367 . . . . . . 7 |- ((x e. A /\ E.v(((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))) <-> (x e. A /\ ((y e. B /\ z e. C) /\ w = (x .Q (y +Q z)))))
31 19.42v 966 . . . . . . 7 |- (E.v(x e. A /\ (((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))) <-> (x e. A /\ E.v(((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))))
32 anass 336 . . . . . . 7 |- (((x e. A /\ (y e. B /\ z e. C)) /\ w = (x .Q (y +Q z))) <-> (x e. A /\ ((y e. B /\ z e. C) /\ w = (x .Q (y +Q z)))))
3330, 31, 323bitr4 158 . . . . . 6 |- (E.v(x e. A /\ (((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))) <-> ((x e. A /\ (y e. B /\ z e. C)) /\ w = (x .Q (y +Q z))))
3433bi3ex 735 . . . . 5 |- (E.yE.zE.xE.v(x e. A /\ (((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))) <-> E.yE.zE.x((x e. A /\ (y e. B /\ z e. C)) /\ w = (x .Q (y +Q z))))
3520, 34bitr 151 . . . 4 |- (E.xE.vE.yE.z(x e. A /\ (((y e. B /\ z e. C) /\ v = (y +Q z)) /\ w = (x .Q v))) <-> E.yE.zE.x((x e. A /\ (y e. B /\ z e. C)) /\ w = (x .Q (y +Q z))))
3619, 35syl6bb 414 . . 3 |- ((A e. P. /\ (B e. P. /\ C e. P.)) -> (w e. (A .P (B +P. C)) <-> E.yE.zE.x((x e. A /\ (y e. B /\ z