Proof of Theorem eigre
Step | Hyp | Ref
| Expression |
1 | | fveq2 6674 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝑇‘𝐴) = (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) |
2 | | oveq2 7178 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐵
·ℎ 𝐴) = (𝐵 ·ℎ if(𝐴 ∈ ℋ, 𝐴,
0ℎ))) |
3 | 1, 2 | eqeq12d 2754 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ↔ (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐵
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))) |
4 | | neeq1 2996 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴 ≠ 0ℎ
↔ if(𝐴 ∈ ℋ,
𝐴, 0ℎ)
≠ 0ℎ)) |
5 | 3, 4 | anbi12d 634 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) ↔ ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐵
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ≠
0ℎ))) |
6 | | id 22 |
. . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → 𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) |
7 | 6, 1 | oveq12d 7188 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴
·ih (𝑇‘𝐴)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))) |
8 | 1, 6 | oveq12d 7188 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝑇‘𝐴) ·ih 𝐴) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) |
9 | 7, 8 | eqeq12d 2754 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝐴
·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))) |
10 | 9 | bibi1d 347 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((𝐴
·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ) ↔ ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ↔ 𝐵 ∈
ℝ))) |
11 | 5, 10 | imbi12d 348 |
. . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) → ((𝐴
·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ)) ↔ (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐵
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ≠
0ℎ) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ↔ 𝐵 ∈
ℝ)))) |
12 | | oveq1 7177 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℂ, 𝐵, 0) → (𝐵 ·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) =
(if(𝐵 ∈ ℂ, 𝐵, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) |
13 | 12 | eqeq2d 2749 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℂ, 𝐵, 0) → ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐵
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ↔ (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐵 ∈ ℂ, 𝐵, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))) |
14 | 13 | anbi1d 633 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℂ, 𝐵, 0) → (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐵
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ≠
0ℎ) ↔ ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐵 ∈ ℂ, 𝐵, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ≠
0ℎ))) |
15 | | eleq1 2820 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℂ, 𝐵, 0) → (𝐵 ∈ ℝ ↔ if(𝐵 ∈ ℂ, 𝐵, 0) ∈ ℝ)) |
16 | 15 | bibi2d 346 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℂ, 𝐵, 0) → (((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ↔ 𝐵 ∈ ℝ) ↔
((if(𝐴 ∈ ℋ,
𝐴, 0ℎ)
·ih (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ↔ if(𝐵 ∈ ℂ, 𝐵, 0) ∈
ℝ))) |
17 | 14, 16 | imbi12d 348 |
. . 3
⊢ (𝐵 = if(𝐵 ∈ ℂ, 𝐵, 0) → ((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐵
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ≠
0ℎ) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ↔ 𝐵 ∈ ℝ)) ↔
(((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) =
(if(𝐵 ∈ ℂ, 𝐵, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ≠
0ℎ) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ↔ if(𝐵 ∈ ℂ, 𝐵, 0) ∈
ℝ)))) |
18 | | ifhvhv0 28957 |
. . . 4
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈
ℋ |
19 | | 0cn 10711 |
. . . . 5
⊢ 0 ∈
ℂ |
20 | 19 | elimel 4483 |
. . . 4
⊢ if(𝐵 ∈ ℂ, 𝐵, 0) ∈
ℂ |
21 | 18, 20 | eigrei 29769 |
. . 3
⊢ (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐵 ∈ ℂ, 𝐵, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ≠
0ℎ) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ↔ if(𝐵 ∈ ℂ, 𝐵, 0) ∈
ℝ)) |
22 | 11, 17, 21 | dedth2h 4473 |
. 2
⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ) → (((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ) → ((𝐴
·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ))) |
23 | 22 | imp 410 |
1
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ) ∧ ((𝑇‘𝐴) = (𝐵 ·ℎ 𝐴) ∧ 𝐴 ≠ 0ℎ)) → ((𝐴
·ih (𝑇‘𝐴)) = ((𝑇‘𝐴) ·ih 𝐴) ↔ 𝐵 ∈ ℝ)) |