Step |
Hyp |
Ref |
Expression |
1 |
|
shincl.1 |
|- A e. SH |
2 |
|
shincl.2 |
|- B e. SH |
3 |
1
|
sheli |
|- ( x e. A -> x e. ~H ) |
4 |
|
ax-hvaddid |
|- ( x e. ~H -> ( x +h 0h ) = x ) |
5 |
4
|
eqcomd |
|- ( x e. ~H -> x = ( x +h 0h ) ) |
6 |
3 5
|
syl |
|- ( x e. A -> x = ( x +h 0h ) ) |
7 |
|
sh0 |
|- ( B e. SH -> 0h e. B ) |
8 |
2 7
|
ax-mp |
|- 0h e. B |
9 |
|
rspceov |
|- ( ( x e. A /\ 0h e. B /\ x = ( x +h 0h ) ) -> E. y e. A E. z e. B x = ( y +h z ) ) |
10 |
8 9
|
mp3an2 |
|- ( ( x e. A /\ x = ( x +h 0h ) ) -> E. y e. A E. z e. B x = ( y +h z ) ) |
11 |
6 10
|
mpdan |
|- ( x e. A -> E. y e. A E. z e. B x = ( y +h z ) ) |
12 |
2
|
sheli |
|- ( x e. B -> x e. ~H ) |
13 |
|
hvaddid2 |
|- ( x e. ~H -> ( 0h +h x ) = x ) |
14 |
13
|
eqcomd |
|- ( x e. ~H -> x = ( 0h +h x ) ) |
15 |
12 14
|
syl |
|- ( x e. B -> x = ( 0h +h x ) ) |
16 |
|
sh0 |
|- ( A e. SH -> 0h e. A ) |
17 |
1 16
|
ax-mp |
|- 0h e. A |
18 |
|
rspceov |
|- ( ( 0h e. A /\ x e. B /\ x = ( 0h +h x ) ) -> E. y e. A E. z e. B x = ( y +h z ) ) |
19 |
17 18
|
mp3an1 |
|- ( ( x e. B /\ x = ( 0h +h x ) ) -> E. y e. A E. z e. B x = ( y +h z ) ) |
20 |
15 19
|
mpdan |
|- ( x e. B -> E. y e. A E. z e. B x = ( y +h z ) ) |
21 |
11 20
|
jaoi |
|- ( ( x e. A \/ x e. B ) -> E. y e. A E. z e. B x = ( y +h z ) ) |
22 |
|
elun |
|- ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) ) |
23 |
1 2
|
shseli |
|- ( x e. ( A +H B ) <-> E. y e. A E. z e. B x = ( y +h z ) ) |
24 |
21 22 23
|
3imtr4i |
|- ( x e. ( A u. B ) -> x e. ( A +H B ) ) |
25 |
24
|
ssriv |
|- ( A u. B ) C_ ( A +H B ) |