| Step |
Hyp |
Ref |
Expression |
| 1 |
|
omlsilem.1 |
|- G e. SH |
| 2 |
|
omlsilem.2 |
|- H e. SH |
| 3 |
|
omlsilem.3 |
|- G C_ H |
| 4 |
|
omlsilem.4 |
|- ( H i^i ( _|_ ` G ) ) = 0H |
| 5 |
|
omlsilem.5 |
|- A e. H |
| 6 |
|
omlsilem.6 |
|- B e. G |
| 7 |
|
omlsilem.7 |
|- C e. ( _|_ ` G ) |
| 8 |
2 5
|
shelii |
|- A e. ~H |
| 9 |
1 6
|
shelii |
|- B e. ~H |
| 10 |
|
shocss |
|- ( G e. SH -> ( _|_ ` G ) C_ ~H ) |
| 11 |
1 10
|
ax-mp |
|- ( _|_ ` G ) C_ ~H |
| 12 |
11 7
|
sselii |
|- C e. ~H |
| 13 |
8 9 12
|
hvsubaddi |
|- ( ( A -h B ) = C <-> ( B +h C ) = A ) |
| 14 |
|
eqcom |
|- ( ( B +h C ) = A <-> A = ( B +h C ) ) |
| 15 |
13 14
|
bitri |
|- ( ( A -h B ) = C <-> A = ( B +h C ) ) |
| 16 |
3 6
|
sselii |
|- B e. H |
| 17 |
|
shsubcl |
|- ( ( H e. SH /\ A e. H /\ B e. H ) -> ( A -h B ) e. H ) |
| 18 |
2 5 16 17
|
mp3an |
|- ( A -h B ) e. H |
| 19 |
|
eleq1 |
|- ( ( A -h B ) = C -> ( ( A -h B ) e. H <-> C e. H ) ) |
| 20 |
18 19
|
mpbii |
|- ( ( A -h B ) = C -> C e. H ) |
| 21 |
15 20
|
sylbir |
|- ( A = ( B +h C ) -> C e. H ) |
| 22 |
4
|
eleq2i |
|- ( C e. ( H i^i ( _|_ ` G ) ) <-> C e. 0H ) |
| 23 |
|
elin |
|- ( C e. ( H i^i ( _|_ ` G ) ) <-> ( C e. H /\ C e. ( _|_ ` G ) ) ) |
| 24 |
|
elch0 |
|- ( C e. 0H <-> C = 0h ) |
| 25 |
22 23 24
|
3bitr3i |
|- ( ( C e. H /\ C e. ( _|_ ` G ) ) <-> C = 0h ) |
| 26 |
21 7 25
|
sylanblc |
|- ( A = ( B +h C ) -> C = 0h ) |
| 27 |
26
|
oveq2d |
|- ( A = ( B +h C ) -> ( B +h C ) = ( B +h 0h ) ) |
| 28 |
|
ax-hvaddid |
|- ( B e. ~H -> ( B +h 0h ) = B ) |
| 29 |
9 28
|
ax-mp |
|- ( B +h 0h ) = B |
| 30 |
27 29
|
eqtrdi |
|- ( A = ( B +h C ) -> ( B +h C ) = B ) |
| 31 |
30 6
|
eqeltrdi |
|- ( A = ( B +h C ) -> ( B +h C ) e. G ) |
| 32 |
|
eleq1 |
|- ( A = ( B +h C ) -> ( A e. G <-> ( B +h C ) e. G ) ) |
| 33 |
31 32
|
mpbird |
|- ( A = ( B +h C ) -> A e. G ) |