Step |
Hyp |
Ref |
Expression |
1 |
|
ax-hv0cl |
|- 0h e. ~H |
2 |
|
snssi |
|- ( 0h e. ~H -> { 0h } C_ ~H ) |
3 |
1 2
|
ax-mp |
|- { 0h } C_ ~H |
4 |
1
|
elexi |
|- 0h e. _V |
5 |
4
|
snid |
|- 0h e. { 0h } |
6 |
3 5
|
pm3.2i |
|- ( { 0h } C_ ~H /\ 0h e. { 0h } ) |
7 |
|
velsn |
|- ( x e. { 0h } <-> x = 0h ) |
8 |
|
velsn |
|- ( y e. { 0h } <-> y = 0h ) |
9 |
|
oveq12 |
|- ( ( x = 0h /\ y = 0h ) -> ( x +h y ) = ( 0h +h 0h ) ) |
10 |
1
|
hvaddid2i |
|- ( 0h +h 0h ) = 0h |
11 |
9 10
|
eqtrdi |
|- ( ( x = 0h /\ y = 0h ) -> ( x +h y ) = 0h ) |
12 |
|
ovex |
|- ( x +h y ) e. _V |
13 |
12
|
elsn |
|- ( ( x +h y ) e. { 0h } <-> ( x +h y ) = 0h ) |
14 |
11 13
|
sylibr |
|- ( ( x = 0h /\ y = 0h ) -> ( x +h y ) e. { 0h } ) |
15 |
7 8 14
|
syl2anb |
|- ( ( x e. { 0h } /\ y e. { 0h } ) -> ( x +h y ) e. { 0h } ) |
16 |
15
|
rgen2 |
|- A. x e. { 0h } A. y e. { 0h } ( x +h y ) e. { 0h } |
17 |
|
oveq2 |
|- ( y = 0h -> ( x .h y ) = ( x .h 0h ) ) |
18 |
|
hvmul0 |
|- ( x e. CC -> ( x .h 0h ) = 0h ) |
19 |
17 18
|
sylan9eqr |
|- ( ( x e. CC /\ y = 0h ) -> ( x .h y ) = 0h ) |
20 |
|
ovex |
|- ( x .h y ) e. _V |
21 |
20
|
elsn |
|- ( ( x .h y ) e. { 0h } <-> ( x .h y ) = 0h ) |
22 |
19 21
|
sylibr |
|- ( ( x e. CC /\ y = 0h ) -> ( x .h y ) e. { 0h } ) |
23 |
8 22
|
sylan2b |
|- ( ( x e. CC /\ y e. { 0h } ) -> ( x .h y ) e. { 0h } ) |
24 |
23
|
rgen2 |
|- A. x e. CC A. y e. { 0h } ( x .h y ) e. { 0h } |
25 |
16 24
|
pm3.2i |
|- ( A. x e. { 0h } A. y e. { 0h } ( x +h y ) e. { 0h } /\ A. x e. CC A. y e. { 0h } ( x .h y ) e. { 0h } ) |
26 |
|
issh2 |
|- ( { 0h } e. SH <-> ( ( { 0h } C_ ~H /\ 0h e. { 0h } ) /\ ( A. x e. { 0h } A. y e. { 0h } ( x +h y ) e. { 0h } /\ A. x e. CC A. y e. { 0h } ( x .h y ) e. { 0h } ) ) ) |
27 |
6 25 26
|
mpbir2an |
|- { 0h } e. SH |
28 |
4
|
fconst2 |
|- ( f : NN --> { 0h } <-> f = ( NN X. { 0h } ) ) |
29 |
|
hlim0 |
|- ( NN X. { 0h } ) ~~>v 0h |
30 |
|
breq1 |
|- ( f = ( NN X. { 0h } ) -> ( f ~~>v 0h <-> ( NN X. { 0h } ) ~~>v 0h ) ) |
31 |
29 30
|
mpbiri |
|- ( f = ( NN X. { 0h } ) -> f ~~>v 0h ) |
32 |
28 31
|
sylbi |
|- ( f : NN --> { 0h } -> f ~~>v 0h ) |
33 |
|
hlimuni |
|- ( ( f ~~>v 0h /\ f ~~>v x ) -> 0h = x ) |
34 |
33
|
eleq1d |
|- ( ( f ~~>v 0h /\ f ~~>v x ) -> ( 0h e. { 0h } <-> x e. { 0h } ) ) |
35 |
32 34
|
sylan |
|- ( ( f : NN --> { 0h } /\ f ~~>v x ) -> ( 0h e. { 0h } <-> x e. { 0h } ) ) |
36 |
5 35
|
mpbii |
|- ( ( f : NN --> { 0h } /\ f ~~>v x ) -> x e. { 0h } ) |
37 |
36
|
gen2 |
|- A. f A. x ( ( f : NN --> { 0h } /\ f ~~>v x ) -> x e. { 0h } ) |
38 |
|
isch2 |
|- ( { 0h } e. CH <-> ( { 0h } e. SH /\ A. f A. x ( ( f : NN --> { 0h } /\ f ~~>v x ) -> x e. { 0h } ) ) ) |
39 |
27 37 38
|
mpbir2an |
|- { 0h } e. CH |