Proof of Theorem eigposi
Step | Hyp | Ref
| Expression |
1 | | oveq2 6557 |
. . . . . . . 8
⊢ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) → (𝐴 ·ih (𝑇‘𝐴)) = (𝐴 ·ih (𝐵
·ℎ 𝐴))) |
2 | 1 | eleq1d 2672 |
. . . . . . 7
⊢ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) → ((𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ ↔ (𝐴 ·ih (𝐵
·ℎ 𝐴)) ∈ ℝ)) |
3 | | oveq1 6556 |
. . . . . . . . 9
⊢ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) → ((𝑇‘𝐴) ·ih 𝐴) = ((𝐵 ·ℎ 𝐴)
·ih 𝐴)) |
4 | 1, 3 | eqeq12d 2625 |
. . . . . . . 8
⊢ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) → ((𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ (𝐴 ·ih (𝐵
·ℎ 𝐴)) = ((𝐵 ·ℎ 𝐴)
·ih 𝐴))) |
5 | | eigpos.1 |
. . . . . . . . 9
⊢ 𝐴 ∈ ℋ |
6 | | eigpos.2 |
. . . . . . . . . 10
⊢ 𝐵 ∈ ℂ |
7 | 6, 5 | hvmulcli 27255 |
. . . . . . . . 9
⊢ (𝐵
·ℎ 𝐴) ∈ ℋ |
8 | | hire 27335 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℋ ∧ (𝐵
·ℎ 𝐴) ∈ ℋ) → ((𝐴 ·ih (𝐵
·ℎ 𝐴)) ∈ ℝ ↔ (𝐴 ·ih (𝐵
·ℎ 𝐴)) = ((𝐵 ·ℎ 𝐴)
·ih 𝐴))) |
9 | 5, 7, 8 | mp2an 704 |
. . . . . . . 8
⊢ ((𝐴
·ih (𝐵 ·ℎ 𝐴)) ∈ ℝ ↔ (𝐴
·ih (𝐵 ·ℎ 𝐴)) = ((𝐵 ·ℎ 𝐴)
·ih 𝐴)) |
10 | 4, 9 | syl6rbbr 278 |
. . . . . . 7
⊢ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) → ((𝐴 ·ih (𝐵
·ℎ 𝐴)) ∈ ℝ ↔ (𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴))) |
11 | 2, 10 | bitrd 267 |
. . . . . 6
⊢ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) → ((𝐴 ·ih (𝑇‘𝐴)) ∈ ℝ ↔ (𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴))) |
12 | 11 | adantr 480 |
. . . . 5
⊢ (((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) → ((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ↔ (𝐴 ·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴))) |
13 | 5, 6 | eigrei 28077 |
. . . . 5
⊢ (((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) → ((𝐴
·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ)) |
14 | 12, 13 | bitrd 267 |
. . . 4
⊢ (((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) → ((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ↔ 𝐵 ∈ ℝ)) |
15 | 14 | biimpac 502 |
. . 3
⊢ (((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → 𝐵 ∈
ℝ) |
16 | 15 | adantlr 747 |
. 2
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → 𝐵 ∈
ℝ) |
17 | | ax-his4 27326 |
. . . . 5
⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ)
→ 0 < (𝐴
·ih 𝐴)) |
18 | 5, 17 | mpan 702 |
. . . 4
⊢ (𝐴 ≠ 0ℎ
→ 0 < (𝐴
·ih 𝐴)) |
19 | 18 | ad2antll 761 |
. . 3
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → 0 <
(𝐴
·ih 𝐴)) |
20 | | simplr 788 |
. . . 4
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → 0 ≤
(𝐴
·ih (𝑇‘𝐴))) |
21 | 1 | ad2antrl 760 |
. . . . 5
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐴
·ih (𝑇‘𝐴)) = (𝐴 ·ih (𝐵
·ℎ 𝐴))) |
22 | | his5 27327 |
. . . . . . 7
⊢ ((𝐵 ∈ ℂ ∧ 𝐴 ∈ ℋ ∧ 𝐴 ∈ ℋ) → (𝐴
·ih (𝐵 ·ℎ 𝐴)) = ((∗‘𝐵) · (𝐴 ·ih 𝐴))) |
23 | 6, 5, 5, 22 | mp3an 1416 |
. . . . . 6
⊢ (𝐴
·ih (𝐵 ·ℎ 𝐴)) = ((∗‘𝐵) · (𝐴 ·ih 𝐴)) |
24 | 16 | cjred 13814 |
. . . . . . 7
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) →
(∗‘𝐵) = 𝐵) |
25 | 24 | oveq1d 6564 |
. . . . . 6
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) →
((∗‘𝐵)
· (𝐴
·ih 𝐴)) = (𝐵 · (𝐴 ·ih 𝐴))) |
26 | 23, 25 | syl5eq 2656 |
. . . . 5
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐴
·ih (𝐵 ·ℎ 𝐴)) = (𝐵 · (𝐴 ·ih 𝐴))) |
27 | 21, 26 | eqtrd 2644 |
. . . 4
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐴
·ih (𝑇‘𝐴)) = (𝐵 · (𝐴 ·ih 𝐴))) |
28 | 20, 27 | breqtrd 4609 |
. . 3
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → 0 ≤
(𝐵 · (𝐴
·ih 𝐴))) |
29 | | hiidrcl 27336 |
. . . . 5
⊢ (𝐴 ∈ ℋ → (𝐴
·ih 𝐴) ∈ ℝ) |
30 | 5, 29 | ax-mp 5 |
. . . 4
⊢ (𝐴
·ih 𝐴) ∈ ℝ |
31 | | prodge02 10750 |
. . . 4
⊢ (((𝐵 ∈ ℝ ∧ (𝐴
·ih 𝐴) ∈ ℝ) ∧ (0 < (𝐴
·ih 𝐴) ∧ 0 ≤ (𝐵 · (𝐴 ·ih 𝐴)))) → 0 ≤ 𝐵) |
32 | 30, 31 | mpanl2 713 |
. . 3
⊢ ((𝐵 ∈ ℝ ∧ (0 <
(𝐴
·ih 𝐴) ∧ 0 ≤ (𝐵 · (𝐴 ·ih 𝐴)))) → 0 ≤ 𝐵) |
33 | 16, 19, 28, 32 | syl12anc 1316 |
. 2
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → 0 ≤
𝐵) |
34 | 16, 33 | jca 553 |
1
⊢ ((((𝐴
·ih (𝑇‘𝐴)) ∈ ℝ ∧ 0 ≤ (𝐴
·ih (𝑇‘𝐴))) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → (𝐵 ∈ ℝ ∧ 0 ≤
𝐵)) |