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