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