Step |
Hyp |
Ref |
Expression |
1 |
|
shsval |
|- ( ( A e. SH /\ B e. SH ) -> ( A +H B ) = ( +h " ( A X. B ) ) ) |
2 |
1
|
eleq2d |
|- ( ( A e. SH /\ B e. SH ) -> ( C e. ( A +H B ) <-> C e. ( +h " ( A X. B ) ) ) ) |
3 |
|
ax-hfvadd |
|- +h : ( ~H X. ~H ) --> ~H |
4 |
|
ffn |
|- ( +h : ( ~H X. ~H ) --> ~H -> +h Fn ( ~H X. ~H ) ) |
5 |
3 4
|
ax-mp |
|- +h Fn ( ~H X. ~H ) |
6 |
|
shss |
|- ( A e. SH -> A C_ ~H ) |
7 |
|
shss |
|- ( B e. SH -> B C_ ~H ) |
8 |
|
xpss12 |
|- ( ( A C_ ~H /\ B C_ ~H ) -> ( A X. B ) C_ ( ~H X. ~H ) ) |
9 |
6 7 8
|
syl2an |
|- ( ( A e. SH /\ B e. SH ) -> ( A X. B ) C_ ( ~H X. ~H ) ) |
10 |
|
ovelimab |
|- ( ( +h Fn ( ~H X. ~H ) /\ ( A X. B ) C_ ( ~H X. ~H ) ) -> ( C e. ( +h " ( A X. B ) ) <-> E. x e. A E. y e. B C = ( x +h y ) ) ) |
11 |
5 9 10
|
sylancr |
|- ( ( A e. SH /\ B e. SH ) -> ( C e. ( +h " ( A X. B ) ) <-> E. x e. A E. y e. B C = ( x +h y ) ) ) |
12 |
2 11
|
bitrd |
|- ( ( A e. SH /\ B e. SH ) -> ( C e. ( A +H B ) <-> E. x e. A E. y e. B C = ( x +h y ) ) ) |