Proof of Theorem eigorth
Step | Hyp | Ref
| Expression |
1 | | fveq2 6674 |
. . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝑇‘𝐴) = (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) |
2 | | oveq2 7178 |
. . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐶
·ℎ 𝐴) = (𝐶 ·ℎ if(𝐴 ∈ ℋ, 𝐴,
0ℎ))) |
3 | 1, 2 | eqeq12d 2754 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ↔ (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))) |
4 | 3 | anbi1d 633 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ↔ ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)))) |
5 | 4 | anbi1d 633 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) ↔ (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)))) |
6 | | oveq1 7177 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴
·ih (𝑇‘𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵))) |
7 | 1 | oveq1d 7185 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝑇‘𝐴) ·ih 𝐵) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵)) |
8 | 6, 7 | eqeq12d 2754 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝐴
·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵)) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵))) |
9 | | oveq1 7177 |
. . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴
·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵)) |
10 | 9 | eqeq1d 2740 |
. . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝐴
·ih 𝐵) = 0 ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0)) |
11 | 8, 10 | bibi12d 349 |
. . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((𝐴
·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0) ↔ ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵)) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0))) |
12 | 5, 11 | imbi12d 348 |
. . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0)) ↔ ((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵)) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0)))) |
13 | | fveq2 6674 |
. . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (𝑇‘𝐵) = (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) |
14 | | oveq2 7178 |
. . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (𝐷
·ℎ 𝐵) = (𝐷 ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))) |
15 | 13, 14 | eqeq12d 2754 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((𝑇‘𝐵) = (𝐷 ·ℎ 𝐵) ↔ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) |
16 | 15 | anbi2d 632 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ↔ ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))) |
17 | 16 | anbi1d 633 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) ↔ (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ∧ 𝐶 ≠ (∗‘𝐷)))) |
18 | 13 | oveq2d 7186 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) |
19 | | oveq2 7178 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) |
20 | 18, 19 | eqeq12d 2754 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵)) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) |
21 | | oveq2 7178 |
. . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) |
22 | 21 | eqeq1d 2740 |
. . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0 ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
0)) |
23 | 20, 22 | bibi12d 349 |
. . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵)) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0) ↔ ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
0))) |
24 | 17, 23 | imbi12d 348 |
. . 3
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵)) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0)) ↔ ((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ∧ 𝐶 ≠ (∗‘𝐷)) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
0)))) |
25 | | oveq1 7177 |
. . . . . . 7
⊢ (𝐶 = if(𝐶 ∈ ℂ, 𝐶, 0) → (𝐶 ·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) =
(if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) |
26 | 25 | eqeq2d 2749 |
. . . . . 6
⊢ (𝐶 = if(𝐶 ∈ ℂ, 𝐶, 0) → ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ↔ (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))) |
27 | 26 | anbi1d 633 |
. . . . 5
⊢ (𝐶 = if(𝐶 ∈ ℂ, 𝐶, 0) → (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ↔ ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))) |
28 | | neeq1 2996 |
. . . . 5
⊢ (𝐶 = if(𝐶 ∈ ℂ, 𝐶, 0) → (𝐶 ≠ (∗‘𝐷) ↔ if(𝐶 ∈ ℂ, 𝐶, 0) ≠ (∗‘𝐷))) |
29 | 27, 28 | anbi12d 634 |
. . . 4
⊢ (𝐶 = if(𝐶 ∈ ℂ, 𝐶, 0) → ((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ∧ 𝐶 ≠ (∗‘𝐷)) ↔ (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ∧ if(𝐶 ∈ ℂ, 𝐶, 0) ≠ (∗‘𝐷)))) |
30 | 29 | imbi1d 345 |
. . 3
⊢ (𝐶 = if(𝐶 ∈ ℂ, 𝐶, 0) → (((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ∧ 𝐶 ≠ (∗‘𝐷)) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = 0)) ↔
((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) =
(if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ∧ if(𝐶 ∈ ℂ, 𝐶, 0) ≠ (∗‘𝐷)) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
0)))) |
31 | | oveq1 7177 |
. . . . . . 7
⊢ (𝐷 = if(𝐷 ∈ ℂ, 𝐷, 0) → (𝐷 ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
(if(𝐷 ∈ ℂ, 𝐷, 0)
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) |
32 | 31 | eqeq2d 2749 |
. . . . . 6
⊢ (𝐷 = if(𝐷 ∈ ℂ, 𝐷, 0) → ((𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) ↔ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (if(𝐷 ∈ ℂ, 𝐷, 0)
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) |
33 | 32 | anbi2d 632 |
. . . . 5
⊢ (𝐷 = if(𝐷 ∈ ℂ, 𝐷, 0) → (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ↔ ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (if(𝐷 ∈ ℂ, 𝐷, 0)
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))) |
34 | | fveq2 6674 |
. . . . . 6
⊢ (𝐷 = if(𝐷 ∈ ℂ, 𝐷, 0) → (∗‘𝐷) = (∗‘if(𝐷 ∈ ℂ, 𝐷, 0))) |
35 | 34 | neeq2d 2994 |
. . . . 5
⊢ (𝐷 = if(𝐷 ∈ ℂ, 𝐷, 0) → (if(𝐶 ∈ ℂ, 𝐶, 0) ≠ (∗‘𝐷) ↔ if(𝐶 ∈ ℂ, 𝐶, 0) ≠ (∗‘if(𝐷 ∈ ℂ, 𝐷, 0)))) |
36 | 33, 35 | anbi12d 634 |
. . . 4
⊢ (𝐷 = if(𝐷 ∈ ℂ, 𝐷, 0) → ((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ∧ if(𝐶 ∈ ℂ, 𝐶, 0) ≠ (∗‘𝐷)) ↔ (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (if(𝐷 ∈ ℂ, 𝐷, 0)
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ∧ if(𝐶 ∈ ℂ, 𝐶, 0) ≠
(∗‘if(𝐷 ∈
ℂ, 𝐷,
0))))) |
37 | 36 | imbi1d 345 |
. . 3
⊢ (𝐷 = if(𝐷 ∈ ℂ, 𝐷, 0) → (((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ∧ if(𝐶 ∈ ℂ, 𝐶, 0) ≠ (∗‘𝐷)) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = 0)) ↔
((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) =
(if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (if(𝐷 ∈ ℂ, 𝐷, 0)
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ∧ if(𝐶 ∈ ℂ, 𝐶, 0) ≠
(∗‘if(𝐷 ∈
ℂ, 𝐷, 0))) →
((if(𝐴 ∈ ℋ,
𝐴, 0ℎ)
·ih (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
0)))) |
38 | | ifhvhv0 28957 |
. . . 4
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈
ℋ |
39 | | ifhvhv0 28957 |
. . . 4
⊢ if(𝐵 ∈ ℋ, 𝐵, 0ℎ) ∈
ℋ |
40 | | 0cn 10711 |
. . . . 5
⊢ 0 ∈
ℂ |
41 | 40 | elimel 4483 |
. . . 4
⊢ if(𝐶 ∈ ℂ, 𝐶, 0) ∈
ℂ |
42 | 40 | elimel 4483 |
. . . 4
⊢ if(𝐷 ∈ ℂ, 𝐷, 0) ∈
ℂ |
43 | 38, 39, 41, 42 | eigorthi 29772 |
. . 3
⊢ ((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (if(𝐷 ∈ ℂ, 𝐷, 0)
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ∧ if(𝐶 ∈ ℂ, 𝐶, 0) ≠
(∗‘if(𝐷 ∈
ℂ, 𝐷, 0))) →
((if(𝐴 ∈ ℋ,
𝐴, 0ℎ)
·ih (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
0)) |
44 | 12, 24, 30, 37, 43 | dedth4h 4475 |
. 2
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) →
((((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0))) |
45 | 44 | imp 410 |
1
⊢ ((((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) ∧ (((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷))) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0)) |