Step |
Hyp |
Ref |
Expression |
1 |
|
hvsubcl |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ) |
2 |
|
his2sub |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) = ( ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ) ) |
3 |
1 2
|
mpd3an3 |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) = ( ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ) ) |
4 |
3
|
eqeq1d |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) = 0 ↔ ( ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ) = 0 ) ) |
5 |
|
his6 |
⊢ ( ( 𝐴 −ℎ 𝐵 ) ∈ ℋ → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) = 0 ↔ ( 𝐴 −ℎ 𝐵 ) = 0ℎ ) ) |
6 |
1 5
|
syl |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝐴 −ℎ 𝐵 ) ·ih ( 𝐴 −ℎ 𝐵 ) ) = 0 ↔ ( 𝐴 −ℎ 𝐵 ) = 0ℎ ) ) |
7 |
4 6
|
bitr3d |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ) = 0 ↔ ( 𝐴 −ℎ 𝐵 ) = 0ℎ ) ) |
8 |
|
hicl |
⊢ ( ( 𝐴 ∈ ℋ ∧ ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ) → ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) ∈ ℂ ) |
9 |
1 8
|
syldan |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) ∈ ℂ ) |
10 |
|
simpr |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → 𝐵 ∈ ℋ ) |
11 |
|
hicl |
⊢ ( ( 𝐵 ∈ ℋ ∧ ( 𝐴 −ℎ 𝐵 ) ∈ ℋ ) → ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ∈ ℂ ) |
12 |
10 1 11
|
syl2anc |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ∈ ℂ ) |
13 |
9 12
|
subeq0ad |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) − ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ) = 0 ↔ ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) = ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ) ) |
14 |
|
hvsubeq0 |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 −ℎ 𝐵 ) = 0ℎ ↔ 𝐴 = 𝐵 ) ) |
15 |
7 13 14
|
3bitr3d |
⊢ ( ( 𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·ih ( 𝐴 −ℎ 𝐵 ) ) = ( 𝐵 ·ih ( 𝐴 −ℎ 𝐵 ) ) ↔ 𝐴 = 𝐵 ) ) |