Step | Hyp | Ref
| Expression |
1 | | 0re 10835 |
. . . . 5
⊢ 0 ∈
ℝ |
2 | | remulcl 10814 |
. . . . 5
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 · 𝐴) ∈ ℝ) |
3 | 1, 2 | mpan 690 |
. . . 4
⊢ (𝐴 ∈ ℝ → (0
· 𝐴) ∈
ℝ) |
4 | | ax-rrecex 10801 |
. . . 4
⊢ (((0
· 𝐴) ∈ ℝ
∧ (0 · 𝐴) ≠
0) → ∃𝑦 ∈
ℝ ((0 · 𝐴)
· 𝑦) =
1) |
5 | 3, 4 | sylan 583 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) →
∃𝑦 ∈ ℝ ((0
· 𝐴) · 𝑦) = 1) |
6 | 5 | adantr 484 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) →
∃𝑦 ∈ ℝ ((0
· 𝐴) · 𝑦) = 1) |
7 | | 00id 11007 |
. . . . 5
⊢ (0 + 0) =
0 |
8 | 7 | oveq2i 7224 |
. . . 4
⊢ (((𝑦 · 𝐴) · 𝐵) · (0 + 0)) = (((𝑦 · 𝐴) · 𝐵) · 0) |
9 | 8 | eqcomi 2746 |
. . 3
⊢ (((𝑦 · 𝐴) · 𝐵) · 0) = (((𝑦 · 𝐴) · 𝐵) · (0 + 0)) |
10 | | simprl 771 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → 𝑦 ∈
ℝ) |
11 | 10 | recnd 10861 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → 𝑦 ∈
ℂ) |
12 | | simplll 775 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → 𝐴 ∈ ℝ) |
13 | 12 | recnd 10861 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → 𝐴 ∈ ℂ) |
14 | 11, 13 | mulcld 10853 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (𝑦 · 𝐴) ∈ ℂ) |
15 | | simplr 769 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → 𝐵 ∈ ℂ) |
16 | | 0cn 10825 |
. . . . . 6
⊢ 0 ∈
ℂ |
17 | | mul32 10998 |
. . . . . 6
⊢ (((𝑦 · 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 0 ∈ ℂ)
→ (((𝑦 · 𝐴) · 𝐵) · 0) = (((𝑦 · 𝐴) · 0) · 𝐵)) |
18 | 16, 17 | mp3an3 1452 |
. . . . 5
⊢ (((𝑦 · 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝑦 · 𝐴) · 𝐵) · 0) = (((𝑦 · 𝐴) · 0) · 𝐵)) |
19 | 14, 15, 18 | syl2anc 587 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (((𝑦 · 𝐴) · 𝐵) · 0) = (((𝑦 · 𝐴) · 0) · 𝐵)) |
20 | | mul31 10999 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → ((𝑦
· 𝐴) · 0) =
((0 · 𝐴) ·
𝑦)) |
21 | 16, 20 | mp3an3 1452 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑦 · 𝐴) · 0) = ((0 · 𝐴) · 𝑦)) |
22 | 11, 13, 21 | syl2anc 587 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → ((𝑦 · 𝐴) · 0) = ((0 · 𝐴) · 𝑦)) |
23 | | simprr 773 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → ((0 ·
𝐴) · 𝑦) = 1) |
24 | 22, 23 | eqtrd 2777 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → ((𝑦 · 𝐴) · 0) = 1) |
25 | 24 | oveq1d 7228 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (((𝑦 · 𝐴) · 0) · 𝐵) = (1 · 𝐵)) |
26 | | mulid2 10832 |
. . . . . 6
⊢ (𝐵 ∈ ℂ → (1
· 𝐵) = 𝐵) |
27 | 26 | ad2antlr 727 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (1 · 𝐵) = 𝐵) |
28 | 25, 27 | eqtrd 2777 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (((𝑦 · 𝐴) · 0) · 𝐵) = 𝐵) |
29 | 19, 28 | eqtrd 2777 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (((𝑦 · 𝐴) · 𝐵) · 0) = 𝐵) |
30 | 14, 15 | mulcld 10853 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → ((𝑦 · 𝐴) · 𝐵) ∈ ℂ) |
31 | | adddi 10818 |
. . . . . 6
⊢ ((((𝑦 · 𝐴) · 𝐵) ∈ ℂ ∧ 0 ∈ ℂ
∧ 0 ∈ ℂ) → (((𝑦 · 𝐴) · 𝐵) · (0 + 0)) = ((((𝑦 · 𝐴) · 𝐵) · 0) + (((𝑦 · 𝐴) · 𝐵) · 0))) |
32 | 16, 16, 31 | mp3an23 1455 |
. . . . 5
⊢ (((𝑦 · 𝐴) · 𝐵) ∈ ℂ → (((𝑦 · 𝐴) · 𝐵) · (0 + 0)) = ((((𝑦 · 𝐴) · 𝐵) · 0) + (((𝑦 · 𝐴) · 𝐵) · 0))) |
33 | 30, 32 | syl 17 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (((𝑦 · 𝐴) · 𝐵) · (0 + 0)) = ((((𝑦 · 𝐴) · 𝐵) · 0) + (((𝑦 · 𝐴) · 𝐵) · 0))) |
34 | 29, 29 | oveq12d 7231 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → ((((𝑦 · 𝐴) · 𝐵) · 0) + (((𝑦 · 𝐴) · 𝐵) · 0)) = (𝐵 + 𝐵)) |
35 | 33, 34 | eqtrd 2777 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (((𝑦 · 𝐴) · 𝐵) · (0 + 0)) = (𝐵 + 𝐵)) |
36 | 9, 29, 35 | 3eqtr3a 2802 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → 𝐵 = (𝐵 + 𝐵)) |
37 | 6, 36 | rexlimddv 3210 |
1
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) →
𝐵 = (𝐵 + 𝐵)) |