Step |
Hyp |
Ref |
Expression |
1 |
|
shintcl.1 |
|- ( A C_ SH /\ A =/= (/) ) |
2 |
1
|
simpri |
|- A =/= (/) |
3 |
|
n0 |
|- ( A =/= (/) <-> E. z z e. A ) |
4 |
|
intss1 |
|- ( z e. A -> |^| A C_ z ) |
5 |
1
|
simpli |
|- A C_ SH |
6 |
5
|
sseli |
|- ( z e. A -> z e. SH ) |
7 |
|
shss |
|- ( z e. SH -> z C_ ~H ) |
8 |
6 7
|
syl |
|- ( z e. A -> z C_ ~H ) |
9 |
4 8
|
sstrd |
|- ( z e. A -> |^| A C_ ~H ) |
10 |
9
|
exlimiv |
|- ( E. z z e. A -> |^| A C_ ~H ) |
11 |
3 10
|
sylbi |
|- ( A =/= (/) -> |^| A C_ ~H ) |
12 |
2 11
|
ax-mp |
|- |^| A C_ ~H |
13 |
|
ax-hv0cl |
|- 0h e. ~H |
14 |
13
|
elexi |
|- 0h e. _V |
15 |
14
|
elint2 |
|- ( 0h e. |^| A <-> A. z e. A 0h e. z ) |
16 |
|
sh0 |
|- ( z e. SH -> 0h e. z ) |
17 |
6 16
|
syl |
|- ( z e. A -> 0h e. z ) |
18 |
15 17
|
mprgbir |
|- 0h e. |^| A |
19 |
12 18
|
pm3.2i |
|- ( |^| A C_ ~H /\ 0h e. |^| A ) |
20 |
|
elinti |
|- ( x e. |^| A -> ( z e. A -> x e. z ) ) |
21 |
20
|
com12 |
|- ( z e. A -> ( x e. |^| A -> x e. z ) ) |
22 |
|
elinti |
|- ( y e. |^| A -> ( z e. A -> y e. z ) ) |
23 |
22
|
com12 |
|- ( z e. A -> ( y e. |^| A -> y e. z ) ) |
24 |
|
shaddcl |
|- ( ( z e. SH /\ x e. z /\ y e. z ) -> ( x +h y ) e. z ) |
25 |
6 24
|
syl3an1 |
|- ( ( z e. A /\ x e. z /\ y e. z ) -> ( x +h y ) e. z ) |
26 |
25
|
3expib |
|- ( z e. A -> ( ( x e. z /\ y e. z ) -> ( x +h y ) e. z ) ) |
27 |
21 23 26
|
syl2and |
|- ( z e. A -> ( ( x e. |^| A /\ y e. |^| A ) -> ( x +h y ) e. z ) ) |
28 |
27
|
com12 |
|- ( ( x e. |^| A /\ y e. |^| A ) -> ( z e. A -> ( x +h y ) e. z ) ) |
29 |
28
|
ralrimiv |
|- ( ( x e. |^| A /\ y e. |^| A ) -> A. z e. A ( x +h y ) e. z ) |
30 |
|
ovex |
|- ( x +h y ) e. _V |
31 |
30
|
elint2 |
|- ( ( x +h y ) e. |^| A <-> A. z e. A ( x +h y ) e. z ) |
32 |
29 31
|
sylibr |
|- ( ( x e. |^| A /\ y e. |^| A ) -> ( x +h y ) e. |^| A ) |
33 |
32
|
rgen2 |
|- A. x e. |^| A A. y e. |^| A ( x +h y ) e. |^| A |
34 |
|
shmulcl |
|- ( ( z e. SH /\ x e. CC /\ y e. z ) -> ( x .h y ) e. z ) |
35 |
6 34
|
syl3an1 |
|- ( ( z e. A /\ x e. CC /\ y e. z ) -> ( x .h y ) e. z ) |
36 |
35
|
3expib |
|- ( z e. A -> ( ( x e. CC /\ y e. z ) -> ( x .h y ) e. z ) ) |
37 |
23 36
|
sylan2d |
|- ( z e. A -> ( ( x e. CC /\ y e. |^| A ) -> ( x .h y ) e. z ) ) |
38 |
37
|
com12 |
|- ( ( x e. CC /\ y e. |^| A ) -> ( z e. A -> ( x .h y ) e. z ) ) |
39 |
38
|
ralrimiv |
|- ( ( x e. CC /\ y e. |^| A ) -> A. z e. A ( x .h y ) e. z ) |
40 |
|
ovex |
|- ( x .h y ) e. _V |
41 |
40
|
elint2 |
|- ( ( x .h y ) e. |^| A <-> A. z e. A ( x .h y ) e. z ) |
42 |
39 41
|
sylibr |
|- ( ( x e. CC /\ y e. |^| A ) -> ( x .h y ) e. |^| A ) |
43 |
42
|
rgen2 |
|- A. x e. CC A. y e. |^| A ( x .h y ) e. |^| A |
44 |
33 43
|
pm3.2i |
|- ( A. x e. |^| A A. y e. |^| A ( x +h y ) e. |^| A /\ A. x e. CC A. y e. |^| A ( x .h y ) e. |^| A ) |
45 |
|
issh2 |
|- ( |^| A e. SH <-> ( ( |^| A C_ ~H /\ 0h e. |^| A ) /\ ( A. x e. |^| A A. y e. |^| A ( x +h y ) e. |^| A /\ A. x e. CC A. y e. |^| A ( x .h y ) e. |^| A ) ) ) |
46 |
19 44 45
|
mpbir2an |
|- |^| A e. SH |