Proof of Theorem hvmul0or
| Step | Hyp | Ref
| Expression |
| 1 | | df-ne 2941 |
. . . . 5
⊢ (𝐴 ≠ 0 ↔ ¬ 𝐴 = 0) |
| 2 | | oveq2 7439 |
. . . . . . . 8
⊢ ((𝐴
·ℎ 𝐵) = 0ℎ → ((1 / 𝐴)
·ℎ (𝐴 ·ℎ 𝐵)) = ((1 / 𝐴) ·ℎ
0ℎ)) |
| 3 | 2 | ad2antlr 727 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ (𝐴
·ℎ 𝐵) = 0ℎ) ∧ 𝐴 ≠ 0) → ((1 / 𝐴)
·ℎ (𝐴 ·ℎ 𝐵)) = ((1 / 𝐴) ·ℎ
0ℎ)) |
| 4 | | recid2 11937 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((1 / 𝐴) · 𝐴) = 1) |
| 5 | 4 | oveq1d 7446 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (((1 / 𝐴) · 𝐴) ·ℎ 𝐵) = (1
·ℎ 𝐵)) |
| 6 | 5 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ 𝐴 ≠ 0) → (((1 / 𝐴) · 𝐴) ·ℎ 𝐵) = (1
·ℎ 𝐵)) |
| 7 | | reccl 11929 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℂ) |
| 8 | 7 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ 𝐴 ≠ 0) → (1 / 𝐴) ∈
ℂ) |
| 9 | | simpll 767 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ 𝐴 ≠ 0) → 𝐴 ∈
ℂ) |
| 10 | | simplr 769 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ 𝐴 ≠ 0) → 𝐵 ∈
ℋ) |
| 11 | | ax-hvmulass 31026 |
. . . . . . . . . 10
⊢ (((1 /
𝐴) ∈ ℂ ∧
𝐴 ∈ ℂ ∧
𝐵 ∈ ℋ) →
(((1 / 𝐴) · 𝐴)
·ℎ 𝐵) = ((1 / 𝐴) ·ℎ (𝐴
·ℎ 𝐵))) |
| 12 | 8, 9, 10, 11 | syl3anc 1373 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ 𝐴 ≠ 0) → (((1 / 𝐴) · 𝐴) ·ℎ 𝐵) = ((1 / 𝐴) ·ℎ (𝐴
·ℎ 𝐵))) |
| 13 | | ax-hvmulid 31025 |
. . . . . . . . . 10
⊢ (𝐵 ∈ ℋ → (1
·ℎ 𝐵) = 𝐵) |
| 14 | 13 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ 𝐴 ≠ 0) → (1
·ℎ 𝐵) = 𝐵) |
| 15 | 6, 12, 14 | 3eqtr3d 2785 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ 𝐴 ≠ 0) → ((1 / 𝐴)
·ℎ (𝐴 ·ℎ 𝐵)) = 𝐵) |
| 16 | 15 | adantlr 715 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ (𝐴
·ℎ 𝐵) = 0ℎ) ∧ 𝐴 ≠ 0) → ((1 / 𝐴)
·ℎ (𝐴 ·ℎ 𝐵)) = 𝐵) |
| 17 | | hvmul0 31043 |
. . . . . . . . . 10
⊢ ((1 /
𝐴) ∈ ℂ →
((1 / 𝐴)
·ℎ 0ℎ) =
0ℎ) |
| 18 | 7, 17 | syl 17 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ((1 / 𝐴)
·ℎ 0ℎ) =
0ℎ) |
| 19 | 18 | adantlr 715 |
. . . . . . . 8
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ 𝐴 ≠ 0) → ((1 / 𝐴)
·ℎ 0ℎ) =
0ℎ) |
| 20 | 19 | adantlr 715 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ (𝐴
·ℎ 𝐵) = 0ℎ) ∧ 𝐴 ≠ 0) → ((1 / 𝐴)
·ℎ 0ℎ) =
0ℎ) |
| 21 | 3, 16, 20 | 3eqtr3d 2785 |
. . . . . 6
⊢ ((((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ (𝐴
·ℎ 𝐵) = 0ℎ) ∧ 𝐴 ≠ 0) → 𝐵 =
0ℎ) |
| 22 | 21 | ex 412 |
. . . . 5
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ (𝐴
·ℎ 𝐵) = 0ℎ) → (𝐴 ≠ 0 → 𝐵 = 0ℎ)) |
| 23 | 1, 22 | biimtrrid 243 |
. . . 4
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ (𝐴
·ℎ 𝐵) = 0ℎ) → (¬
𝐴 = 0 → 𝐵 =
0ℎ)) |
| 24 | 23 | orrd 864 |
. . 3
⊢ (((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) ∧ (𝐴
·ℎ 𝐵) = 0ℎ) → (𝐴 = 0 ∨ 𝐵 = 0ℎ)) |
| 25 | 24 | ex 412 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((𝐴
·ℎ 𝐵) = 0ℎ → (𝐴 = 0 ∨ 𝐵 = 0ℎ))) |
| 26 | | ax-hvmul0 31029 |
. . . . 5
⊢ (𝐵 ∈ ℋ → (0
·ℎ 𝐵) = 0ℎ) |
| 27 | | oveq1 7438 |
. . . . . 6
⊢ (𝐴 = 0 → (𝐴 ·ℎ 𝐵) = (0
·ℎ 𝐵)) |
| 28 | 27 | eqeq1d 2739 |
. . . . 5
⊢ (𝐴 = 0 → ((𝐴 ·ℎ 𝐵) = 0ℎ ↔
(0 ·ℎ 𝐵) = 0ℎ)) |
| 29 | 26, 28 | syl5ibrcom 247 |
. . . 4
⊢ (𝐵 ∈ ℋ → (𝐴 = 0 → (𝐴 ·ℎ 𝐵) =
0ℎ)) |
| 30 | 29 | adantl 481 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐴 = 0 → (𝐴 ·ℎ 𝐵) =
0ℎ)) |
| 31 | | hvmul0 31043 |
. . . . 5
⊢ (𝐴 ∈ ℂ → (𝐴
·ℎ 0ℎ) =
0ℎ) |
| 32 | | oveq2 7439 |
. . . . . 6
⊢ (𝐵 = 0ℎ →
(𝐴
·ℎ 𝐵) = (𝐴 ·ℎ
0ℎ)) |
| 33 | 32 | eqeq1d 2739 |
. . . . 5
⊢ (𝐵 = 0ℎ →
((𝐴
·ℎ 𝐵) = 0ℎ ↔ (𝐴
·ℎ 0ℎ) =
0ℎ)) |
| 34 | 31, 33 | syl5ibrcom 247 |
. . . 4
⊢ (𝐴 ∈ ℂ → (𝐵 = 0ℎ →
(𝐴
·ℎ 𝐵) = 0ℎ)) |
| 35 | 34 | adantr 480 |
. . 3
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → (𝐵 = 0ℎ →
(𝐴
·ℎ 𝐵) = 0ℎ)) |
| 36 | 30, 35 | jaod 860 |
. 2
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((𝐴 = 0 ∨ 𝐵 = 0ℎ) → (𝐴
·ℎ 𝐵) = 0ℎ)) |
| 37 | 25, 36 | impbid 212 |
1
⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℋ) → ((𝐴
·ℎ 𝐵) = 0ℎ ↔ (𝐴 = 0 ∨ 𝐵 = 0ℎ))) |