HomeHome Metamath Proof Explorer < Previous   Next >
Related theorems
Unicode version
Theorem distrlem1pr 5114
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 5076 . . . . . . 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 1811 . . . . . . 7 |- w e. V
31, 2genpelv 5090 . . . . . 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 5107 . . . . . 6 |- ((B e. P. /\ C e. P.) -> (B +P. C) e. P.)
53, 4sylan2 451 . . . . 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 5075 . . . . . . . . . . 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 1811 . . . . . . . . . . 11 |- v e. V
86, 7genpelv 5090 . . . . . . . . . 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 616 . . . . . . . . 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 615 . . . . . . . 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 439 . . . . . . . 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 1310 . . . . . . . . 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 1306 . . . . . . . . . 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 480 . . . . . . . . 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 173 . . . . . . . 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 554 . . . . . . 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 388 . . . . . 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)))))
18172exbidv 1281 . . . . 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 527 . . . 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 1099 . . . . 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 439 . . . . . . . . . 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))))
2221exbii 1050 . . . . . . . . 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 1308 . . . . . . . . 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 3980 . . . . . . . . . . 11 |- (y +Q z) e. V
25 opreq2 3966 . . . . . . . . . . . 12 |- (v = (y +Q z) -> (x .Q v) = (x .Q (y +Q z)))
2625eqeq2d 1485 . . . . . . . . . . 11 |- (v = (y +Q z) -> (w = (x .Q v) <-> w = (x .Q (y +Q z))))
2724, 26ceqsexv 1833 . . . . . . . . . 10 |- (E.v(v = (y +Q z) /\ w = (x .Q v)) <-> w = (x .Q (y +Q z)))
2827anbi2i 480 . . . . . . . . 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 177 . . . . . . . 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 480 . . . . . . 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 1308 . . . . . . 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 439 . . . . . . 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 183 . . . . . 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))))
34333exbi 1052 . . . . 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 173 . . . 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 535 . . 3 |- (