Step |
Hyp |
Ref |
Expression |
1 |
|
an4 |
|- ( ( ( x e. A /\ z e. A ) /\ ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) ) <-> ( ( x e. A /\ E. y e. B C = ( x +h y ) ) /\ ( z e. A /\ E. w e. B C = ( z +h w ) ) ) ) |
2 |
|
reeanv |
|- ( E. y e. B E. w e. B ( C = ( x +h y ) /\ C = ( z +h w ) ) <-> ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) ) |
3 |
|
simpll1 |
|- ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> A e. SH ) |
4 |
|
simpll2 |
|- ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> B e. SH ) |
5 |
|
simpll3 |
|- ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> ( A i^i B ) = 0H ) |
6 |
|
simplrl |
|- ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> x e. A ) |
7 |
|
simprll |
|- ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> y e. B ) |
8 |
|
simplrr |
|- ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> z e. A ) |
9 |
|
simprlr |
|- ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> w e. B ) |
10 |
|
simprrl |
|- ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> C = ( x +h y ) ) |
11 |
|
simprrr |
|- ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> C = ( z +h w ) ) |
12 |
10 11
|
eqtr3d |
|- ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> ( x +h y ) = ( z +h w ) ) |
13 |
3 4 5 6 7 8 9 12
|
shuni |
|- ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> ( x = z /\ y = w ) ) |
14 |
13
|
simpld |
|- ( ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) /\ ( ( y e. B /\ w e. B ) /\ ( C = ( x +h y ) /\ C = ( z +h w ) ) ) ) -> x = z ) |
15 |
14
|
exp32 |
|- ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) -> ( ( y e. B /\ w e. B ) -> ( ( C = ( x +h y ) /\ C = ( z +h w ) ) -> x = z ) ) ) |
16 |
15
|
rexlimdvv |
|- ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) -> ( E. y e. B E. w e. B ( C = ( x +h y ) /\ C = ( z +h w ) ) -> x = z ) ) |
17 |
2 16
|
syl5bir |
|- ( ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) /\ ( x e. A /\ z e. A ) ) -> ( ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) -> x = z ) ) |
18 |
17
|
expimpd |
|- ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) -> ( ( ( x e. A /\ z e. A ) /\ ( E. y e. B C = ( x +h y ) /\ E. w e. B C = ( z +h w ) ) ) -> x = z ) ) |
19 |
1 18
|
syl5bir |
|- ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) -> ( ( ( x e. A /\ E. y e. B C = ( x +h y ) ) /\ ( z e. A /\ E. w e. B C = ( z +h w ) ) ) -> x = z ) ) |
20 |
19
|
alrimivv |
|- ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) -> A. x A. z ( ( ( x e. A /\ E. y e. B C = ( x +h y ) ) /\ ( z e. A /\ E. w e. B C = ( z +h w ) ) ) -> x = z ) ) |
21 |
|
eleq1w |
|- ( x = z -> ( x e. A <-> z e. A ) ) |
22 |
|
oveq1 |
|- ( x = z -> ( x +h y ) = ( z +h y ) ) |
23 |
22
|
eqeq2d |
|- ( x = z -> ( C = ( x +h y ) <-> C = ( z +h y ) ) ) |
24 |
23
|
rexbidv |
|- ( x = z -> ( E. y e. B C = ( x +h y ) <-> E. y e. B C = ( z +h y ) ) ) |
25 |
|
oveq2 |
|- ( y = w -> ( z +h y ) = ( z +h w ) ) |
26 |
25
|
eqeq2d |
|- ( y = w -> ( C = ( z +h y ) <-> C = ( z +h w ) ) ) |
27 |
26
|
cbvrexvw |
|- ( E. y e. B C = ( z +h y ) <-> E. w e. B C = ( z +h w ) ) |
28 |
24 27
|
syl6bb |
|- ( x = z -> ( E. y e. B C = ( x +h y ) <-> E. w e. B C = ( z +h w ) ) ) |
29 |
21 28
|
anbi12d |
|- ( x = z -> ( ( x e. A /\ E. y e. B C = ( x +h y ) ) <-> ( z e. A /\ E. w e. B C = ( z +h w ) ) ) ) |
30 |
29
|
mo4 |
|- ( E* x ( x e. A /\ E. y e. B C = ( x +h y ) ) <-> A. x A. z ( ( ( x e. A /\ E. y e. B C = ( x +h y ) ) /\ ( z e. A /\ E. w e. B C = ( z +h w ) ) ) -> x = z ) ) |
31 |
20 30
|
sylibr |
|- ( ( A e. SH /\ B e. SH /\ ( A i^i B ) = 0H ) -> E* x ( x e. A /\ E. y e. B C = ( x +h y ) ) ) |