Step |
Hyp |
Ref |
Expression |
1 |
|
hvsubcl |
|- ( ( A e. ~H /\ B e. ~H ) -> ( A -h B ) e. ~H ) |
2 |
|
his2sub |
|- ( ( A e. ~H /\ B e. ~H /\ ( A -h B ) e. ~H ) -> ( ( A -h B ) .ih ( A -h B ) ) = ( ( A .ih ( A -h B ) ) - ( B .ih ( A -h B ) ) ) ) |
3 |
1 2
|
mpd3an3 |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A -h B ) .ih ( A -h B ) ) = ( ( A .ih ( A -h B ) ) - ( B .ih ( A -h B ) ) ) ) |
4 |
3
|
eqeq1d |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( ( A -h B ) .ih ( A -h B ) ) = 0 <-> ( ( A .ih ( A -h B ) ) - ( B .ih ( A -h B ) ) ) = 0 ) ) |
5 |
|
his6 |
|- ( ( A -h B ) e. ~H -> ( ( ( A -h B ) .ih ( A -h B ) ) = 0 <-> ( A -h B ) = 0h ) ) |
6 |
1 5
|
syl |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( ( A -h B ) .ih ( A -h B ) ) = 0 <-> ( A -h B ) = 0h ) ) |
7 |
4 6
|
bitr3d |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( ( A .ih ( A -h B ) ) - ( B .ih ( A -h B ) ) ) = 0 <-> ( A -h B ) = 0h ) ) |
8 |
|
hicl |
|- ( ( A e. ~H /\ ( A -h B ) e. ~H ) -> ( A .ih ( A -h B ) ) e. CC ) |
9 |
1 8
|
syldan |
|- ( ( A e. ~H /\ B e. ~H ) -> ( A .ih ( A -h B ) ) e. CC ) |
10 |
|
simpr |
|- ( ( A e. ~H /\ B e. ~H ) -> B e. ~H ) |
11 |
|
hicl |
|- ( ( B e. ~H /\ ( A -h B ) e. ~H ) -> ( B .ih ( A -h B ) ) e. CC ) |
12 |
10 1 11
|
syl2anc |
|- ( ( A e. ~H /\ B e. ~H ) -> ( B .ih ( A -h B ) ) e. CC ) |
13 |
9 12
|
subeq0ad |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( ( A .ih ( A -h B ) ) - ( B .ih ( A -h B ) ) ) = 0 <-> ( A .ih ( A -h B ) ) = ( B .ih ( A -h B ) ) ) ) |
14 |
|
hvsubeq0 |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A -h B ) = 0h <-> A = B ) ) |
15 |
7 13 14
|
3bitr3d |
|- ( ( A e. ~H /\ B e. ~H ) -> ( ( A .ih ( A -h B ) ) = ( B .ih ( A -h B ) ) <-> A = B ) ) |