Proof of Theorem eigorth
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fveq2 6906 | . . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝑇‘𝐴) = (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) | 
| 2 |  | oveq2 7439 | . . . . . . 7
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐶
·ℎ 𝐴) = (𝐶 ·ℎ if(𝐴 ∈ ℋ, 𝐴,
0ℎ))) | 
| 3 | 1, 2 | eqeq12d 2753 | . . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ↔ (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))) | 
| 4 | 3 | anbi1d 631 | . . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ↔ ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)))) | 
| 5 | 4 | anbi1d 631 | . . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) ↔ (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)))) | 
| 6 |  | oveq1 7438 | . . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴
·ih (𝑇‘𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵))) | 
| 7 | 1 | oveq1d 7446 | . . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝑇‘𝐴) ·ih 𝐵) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵)) | 
| 8 | 6, 7 | eqeq12d 2753 | . . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝐴
·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵)) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵))) | 
| 9 |  | oveq1 7438 | . . . . . 6
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (𝐴
·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵)) | 
| 10 | 9 | eqeq1d 2739 | . . . . 5
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → ((𝐴
·ih 𝐵) = 0 ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0)) | 
| 11 | 8, 10 | bibi12d 345 | . . . 4
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((𝐴
·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0) ↔ ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵)) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0))) | 
| 12 | 5, 11 | imbi12d 344 | . . 3
⊢ (𝐴 = if(𝐴 ∈ ℋ, 𝐴, 0ℎ) → (((((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0)) ↔ ((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵)) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0)))) | 
| 13 |  | fveq2 6906 | . . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (𝑇‘𝐵) = (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) | 
| 14 |  | oveq2 7439 | . . . . . . 7
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (𝐷
·ℎ 𝐵) = (𝐷 ·ℎ if(𝐵 ∈ ℋ, 𝐵,
0ℎ))) | 
| 15 | 13, 14 | eqeq12d 2753 | . . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((𝑇‘𝐵) = (𝐷 ·ℎ 𝐵) ↔ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) | 
| 16 | 15 | anbi2d 630 | . . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ↔ ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))) | 
| 17 | 16 | anbi1d 631 | . . . 4
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) ↔ (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ∧ 𝐶 ≠ (∗‘𝐷)))) | 
| 18 | 13 | oveq2d 7447 | . . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵)) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) | 
| 19 |  | oveq2 7439 | . . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) | 
| 20 | 18, 19 | eqeq12d 2753 | . . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘𝐵)) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih 𝐵) ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) = ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ))
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) | 
| 21 |  | oveq2 7439 | . . . . . 6
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) | 
| 22 | 21 | eqeq1d 2739 | . . . . 5
⊢ (𝐵 = if(𝐵 ∈ ℋ, 𝐵, 0ℎ) → ((if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih 𝐵) = 0 ↔ (if(𝐴 ∈ ℋ, 𝐴, 0ℎ)
·ih if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
0)) | 
| 23 | 20, 22 | bibi12d 345 | . . . 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 344 | . . 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 7438 | . . . . . . 7
⊢ (𝐶 = if(𝐶 ∈ ℂ, 𝐶, 0) → (𝐶 ·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) =
(if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ))) | 
| 26 | 25 | eqeq2d 2748 | . . . . . 6
⊢ (𝐶 = if(𝐶 ∈ ℂ, 𝐶, 0) → ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ↔ (𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)))) | 
| 27 | 26 | anbi1d 631 | . . . . 5
⊢ (𝐶 = if(𝐶 ∈ ℂ, 𝐶, 0) → (((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (𝐶
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) ↔ ((𝑇‘if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) = (if(𝐶 ∈ ℂ, 𝐶, 0)
·ℎ if(𝐴 ∈ ℋ, 𝐴, 0ℎ)) ∧ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))))) | 
| 28 |  | neeq1 3003 | . . . . 5
⊢ (𝐶 = if(𝐶 ∈ ℂ, 𝐶, 0) → (𝐶 ≠ (∗‘𝐷) ↔ if(𝐶 ∈ ℂ, 𝐶, 0) ≠ (∗‘𝐷))) | 
| 29 | 27, 28 | anbi12d 632 | . . . 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 341 | . . 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 7438 | . . . . . . 7
⊢ (𝐷 = if(𝐷 ∈ ℂ, 𝐷, 0) → (𝐷 ·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) =
(if(𝐷 ∈ ℂ, 𝐷, 0)
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ))) | 
| 32 | 31 | eqeq2d 2748 | . . . . . 6
⊢ (𝐷 = if(𝐷 ∈ ℂ, 𝐷, 0) → ((𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (𝐷
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) ↔ (𝑇‘if(𝐵 ∈ ℋ, 𝐵, 0ℎ)) = (if(𝐷 ∈ ℂ, 𝐷, 0)
·ℎ if(𝐵 ∈ ℋ, 𝐵, 0ℎ)))) | 
| 33 | 32 | anbi2d 630 | . . . . 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 6906 | . . . . . 6
⊢ (𝐷 = if(𝐷 ∈ ℂ, 𝐷, 0) → (∗‘𝐷) = (∗‘if(𝐷 ∈ ℂ, 𝐷, 0))) | 
| 35 | 34 | neeq2d 3001 | . . . . 5
⊢ (𝐷 = if(𝐷 ∈ ℂ, 𝐷, 0) → (if(𝐶 ∈ ℂ, 𝐶, 0) ≠ (∗‘𝐷) ↔ if(𝐶 ∈ ℂ, 𝐶, 0) ≠ (∗‘if(𝐷 ∈ ℂ, 𝐷, 0)))) | 
| 36 | 33, 35 | anbi12d 632 | . . . 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 341 | . . 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 31041 | . . . 4
⊢ if(𝐴 ∈ ℋ, 𝐴, 0ℎ) ∈
ℋ | 
| 39 |  | ifhvhv0 31041 | . . . 4
⊢ if(𝐵 ∈ ℋ, 𝐵, 0ℎ) ∈
ℋ | 
| 40 |  | 0cn 11253 | . . . . 5
⊢ 0 ∈
ℂ | 
| 41 | 40 | elimel 4595 | . . . 4
⊢ if(𝐶 ∈ ℂ, 𝐶, 0) ∈
ℂ | 
| 42 | 40 | elimel 4595 | . . . 4
⊢ if(𝐷 ∈ ℂ, 𝐷, 0) ∈
ℂ | 
| 43 | 38, 39, 41, 42 | eigorthi 31856 | . . 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 4587 | . 2
⊢ (((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) →
((((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷)) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0))) | 
| 45 | 44 | imp 406 | 1
⊢ ((((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ ℂ ∧ 𝐷 ∈ ℂ)) ∧ (((𝑇‘𝐴) = (𝐶 ·ℎ 𝐴) ∧ (𝑇‘𝐵) = (𝐷 ·ℎ 𝐵)) ∧ 𝐶 ≠ (∗‘𝐷))) → ((𝐴 ·ih (𝑇‘𝐵)) = ((𝑇‘𝐴) ·ih 𝐵) ↔ (𝐴 ·ih 𝐵) = 0)) |