Step | Hyp | Ref
| Expression |
1 | | 0re 11157 |
. . . . 5
⊢ 0 ∈
ℝ |
2 | | remulcl 11136 |
. . . . 5
⊢ ((0
∈ ℝ ∧ 𝐴
∈ ℝ) → (0 · 𝐴) ∈ ℝ) |
3 | 1, 2 | mpan 688 |
. . . 4
⊢ (𝐴 ∈ ℝ → (0
· 𝐴) ∈
ℝ) |
4 | | ax-rrecex 11123 |
. . . 4
⊢ (((0
· 𝐴) ∈ ℝ
∧ (0 · 𝐴) ≠
0) → ∃𝑦 ∈
ℝ ((0 · 𝐴)
· 𝑦) =
1) |
5 | 3, 4 | sylan 580 |
. . 3
⊢ ((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) →
∃𝑦 ∈ ℝ ((0
· 𝐴) · 𝑦) = 1) |
6 | 5 | adantr 481 |
. 2
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) →
∃𝑦 ∈ ℝ ((0
· 𝐴) · 𝑦) = 1) |
7 | | 00id 11330 |
. . . . 5
⊢ (0 + 0) =
0 |
8 | 7 | oveq2i 7368 |
. . . 4
⊢ (((𝑦 · 𝐴) · 𝐵) · (0 + 0)) = (((𝑦 · 𝐴) · 𝐵) · 0) |
9 | 8 | eqcomi 2745 |
. . 3
⊢ (((𝑦 · 𝐴) · 𝐵) · 0) = (((𝑦 · 𝐴) · 𝐵) · (0 + 0)) |
10 | | simprl 769 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → 𝑦 ∈
ℝ) |
11 | 10 | recnd 11183 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → 𝑦 ∈
ℂ) |
12 | | simplll 773 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → 𝐴 ∈ ℝ) |
13 | 12 | recnd 11183 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → 𝐴 ∈ ℂ) |
14 | 11, 13 | mulcld 11175 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (𝑦 · 𝐴) ∈ ℂ) |
15 | | simplr 767 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → 𝐵 ∈ ℂ) |
16 | | 0cn 11147 |
. . . . . 6
⊢ 0 ∈
ℂ |
17 | | mul32 11321 |
. . . . . 6
⊢ (((𝑦 · 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 0 ∈ ℂ)
→ (((𝑦 · 𝐴) · 𝐵) · 0) = (((𝑦 · 𝐴) · 0) · 𝐵)) |
18 | 16, 17 | mp3an3 1450 |
. . . . 5
⊢ (((𝑦 · 𝐴) ∈ ℂ ∧ 𝐵 ∈ ℂ) → (((𝑦 · 𝐴) · 𝐵) · 0) = (((𝑦 · 𝐴) · 0) · 𝐵)) |
19 | 14, 15, 18 | syl2anc 584 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (((𝑦 · 𝐴) · 𝐵) · 0) = (((𝑦 · 𝐴) · 0) · 𝐵)) |
20 | | mul31 11322 |
. . . . . . . . 9
⊢ ((𝑦 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 0 ∈
ℂ) → ((𝑦
· 𝐴) · 0) =
((0 · 𝐴) ·
𝑦)) |
21 | 16, 20 | mp3an3 1450 |
. . . . . . . 8
⊢ ((𝑦 ∈ ℂ ∧ 𝐴 ∈ ℂ) → ((𝑦 · 𝐴) · 0) = ((0 · 𝐴) · 𝑦)) |
22 | 11, 13, 21 | syl2anc 584 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → ((𝑦 · 𝐴) · 0) = ((0 · 𝐴) · 𝑦)) |
23 | | simprr 771 |
. . . . . . 7
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → ((0 ·
𝐴) · 𝑦) = 1) |
24 | 22, 23 | eqtrd 2776 |
. . . . . 6
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → ((𝑦 · 𝐴) · 0) = 1) |
25 | 24 | oveq1d 7372 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (((𝑦 · 𝐴) · 0) · 𝐵) = (1 · 𝐵)) |
26 | | mulid2 11154 |
. . . . . 6
⊢ (𝐵 ∈ ℂ → (1
· 𝐵) = 𝐵) |
27 | 26 | ad2antlr 725 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (1 · 𝐵) = 𝐵) |
28 | 25, 27 | eqtrd 2776 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (((𝑦 · 𝐴) · 0) · 𝐵) = 𝐵) |
29 | 19, 28 | eqtrd 2776 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (((𝑦 · 𝐴) · 𝐵) · 0) = 𝐵) |
30 | 14, 15 | mulcld 11175 |
. . . . 5
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → ((𝑦 · 𝐴) · 𝐵) ∈ ℂ) |
31 | | adddi 11140 |
. . . . . 6
⊢ ((((𝑦 · 𝐴) · 𝐵) ∈ ℂ ∧ 0 ∈ ℂ
∧ 0 ∈ ℂ) → (((𝑦 · 𝐴) · 𝐵) · (0 + 0)) = ((((𝑦 · 𝐴) · 𝐵) · 0) + (((𝑦 · 𝐴) · 𝐵) · 0))) |
32 | 16, 16, 31 | mp3an23 1453 |
. . . . 5
⊢ (((𝑦 · 𝐴) · 𝐵) ∈ ℂ → (((𝑦 · 𝐴) · 𝐵) · (0 + 0)) = ((((𝑦 · 𝐴) · 𝐵) · 0) + (((𝑦 · 𝐴) · 𝐵) · 0))) |
33 | 30, 32 | syl 17 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (((𝑦 · 𝐴) · 𝐵) · (0 + 0)) = ((((𝑦 · 𝐴) · 𝐵) · 0) + (((𝑦 · 𝐴) · 𝐵) · 0))) |
34 | 29, 29 | oveq12d 7375 |
. . . 4
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → ((((𝑦 · 𝐴) · 𝐵) · 0) + (((𝑦 · 𝐴) · 𝐵) · 0)) = (𝐵 + 𝐵)) |
35 | 33, 34 | eqtrd 2776 |
. . 3
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → (((𝑦 · 𝐴) · 𝐵) · (0 + 0)) = (𝐵 + 𝐵)) |
36 | 9, 29, 35 | 3eqtr3a 2800 |
. 2
⊢ ((((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) ∧
(𝑦 ∈ ℝ ∧ ((0
· 𝐴) · 𝑦) = 1)) → 𝐵 = (𝐵 + 𝐵)) |
37 | 6, 36 | rexlimddv 3158 |
1
⊢ (((𝐴 ∈ ℝ ∧ (0
· 𝐴) ≠ 0) ∧
𝐵 ∈ ℂ) →
𝐵 = (𝐵 + 𝐵)) |