Proof of Theorem eigposi
Step | Hyp | Ref
| Expression |
1 | | oveq2 7024 |
. . . . . . . 8
⊢ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) → (𝐴 ·ih (𝑇‘𝐴)) = (𝐴 ·ih (𝐵
·ℎ 𝐴))) |
2 | 1 | eleq1d 2867 |
. . . . . . 7
⊢ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) → ((𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ ↔ (𝐴 ·ih (𝐵
·ℎ 𝐴)) ∈ ℝ)) |
3 | | oveq1 7023 |
. . . . . . . . 9
⊢ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) → ((𝑇‘𝐴) ·ih 𝐴) = ((𝐵 ·ℎ 𝐴)
·ih 𝐴)) |
4 | 1, 3 | eqeq12d 2810 |
. . . . . . . 8
⊢ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) → ((𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ (𝐴 ·ih (𝐵
·ℎ 𝐴)) = ((𝐵 ·ℎ 𝐴)
·ih 𝐴))) |
5 | | eigpos.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ ℋ |
6 | | eigpos.2 |
. . . . . . . . . 10
⊢ 𝐵 ∈ ℂ |
7 | 6, 5 | hvmulcli 28482 |
. . . . . . . . 9
⊢ (𝐵
·ℎ 𝐴) ∈ ℋ |
8 | | hire 28562 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℋ ∧ (𝐵
·ℎ 𝐴) ∈ ℋ) → ((𝐴 ·ih (𝐵
·ℎ 𝐴)) ∈ ℝ ↔ (𝐴 ·ih (𝐵
·ℎ 𝐴)) = ((𝐵 ·ℎ 𝐴)
·ih 𝐴))) |
9 | 5, 7, 8 | mp2an 688 |
. . . . . . . 8
⊢ ((𝐴
·ih (𝐵 ·ℎ 𝐴)) ∈ ℝ ↔ (𝐴
·ih (𝐵 ·ℎ 𝐴)) = ((𝐵 ·ℎ 𝐴)
·ih 𝐴)) |
10 | 4, 9 | syl6rbbr 291 |
. . . . . . 7
⊢ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) → ((𝐴 ·ih (𝐵
·ℎ 𝐴)) ∈ ℝ ↔ (𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴))) |
11 | 2, 10 | bitrd 280 |
. . . . . 6
⊢ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) → ((𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ ↔ (𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴))) |
12 | 11 | adantr 481 |
. . . . 5
⊢ (((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) → ((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ↔ (𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴))) |
13 | 5, 6 | eigrei 29302 |
. . . . 5
⊢ (((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) → ((𝐴
·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ)) |
14 | 12, 13 | bitrd 280 |
. . . 4
⊢ (((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) → ((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ↔ 𝐵 ∈ ℝ)) |
15 | 14 | biimpac 479 |
. . 3
⊢ (((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → 𝐵 ∈
ℝ) |
16 | 15 | adantlr 711 |
. 2
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → 𝐵 ∈
ℝ) |
17 | | hiidrcl 28563 |
. . . . 5
⊢ (𝐴 ∈ ℋ → (𝐴
·ih 𝐴) ∈ ℝ) |
18 | 5, 17 | mp1i 13 |
. . . 4
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐴
·ih 𝐴) ∈ ℝ) |
19 | | ax-his4 28553 |
. . . . . 6
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 0 < (𝐴
·ih 𝐴)) |
20 | 5, 19 | mpan 686 |
. . . . 5
⊢ (𝐴 ≠ 0ℎ
→ 0 < (𝐴
·ih 𝐴)) |
21 | 20 | ad2antll 725 |
. . . 4
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → 0 <
(𝐴
·ih 𝐴)) |
22 | 18, 21 | elrpd 12278 |
. . 3
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐴
·ih 𝐴) ∈
ℝ+) |
23 | | simplr 765 |
. . . 4
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → 0 ≤
(𝐴
·ih (𝑇‘𝐴))) |
24 | 1 | ad2antrl 724 |
. . . . 5
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐴
·ih (𝑇‘𝐴)) = (𝐴 ·ih (𝐵
·ℎ 𝐴))) |
25 | | his5 28554 |
. . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐴
·ih (𝐵 ·ℎ 𝐴)) = ((∗‘𝐵) · (𝐴 ·ih 𝐴))) |
26 | 6, 5, 5, 25 | mp3an 1453 |
. . . . . 6
⊢ (𝐴
·ih (𝐵 ·ℎ 𝐴)) = ((∗‘𝐵) · (𝐴 ·ih 𝐴)) |
27 | 16 | cjred 14419 |
. . . . . . 7
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) →
(∗‘𝐵) = 𝐵) |
28 | 27 | oveq1d 7031 |
. . . . . 6
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) →
((∗‘𝐵)
· (𝐴
·ih 𝐴)) = (𝐵 · (𝐴 ·ih 𝐴))) |
29 | 26, 28 | syl5eq 2843 |
. . . . 5
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐴
·ih (𝐵 ·ℎ 𝐴)) = (𝐵 · (𝐴 ·ih 𝐴))) |
30 | 24, 29 | eqtrd 2831 |
. . . 4
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐴
·ih (𝑇‘𝐴)) = (𝐵 · (𝐴 ·ih 𝐴))) |
31 | 23, 30 | breqtrd 4988 |
. . 3
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → 0 ≤
(𝐵 · (𝐴
·ih 𝐴))) |
32 | 16, 22, 31 | prodge0ld 12347 |
. 2
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → 0 ≤
𝐵) |
33 | 16, 32 | jca 512 |
1
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐵 ∈ ℝ ∧ 0 ≤
𝐵)) |