This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem mul02lem1

Description: Lemma for mul02 . If any real does not produce 0 when multiplied by 0 , then any complex is equal to double itself. (Contributed by Scott Fenton, 3-Jan-2013)

Ref Expression
Assertion mul02lem1 ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → 𝐵 = ( 𝐵 + 𝐵 ) )

Proof

Step Hyp Ref Expression
1 0re ⊢ 0 ∈ ℝ
2 remulcl ⊢ ( ( 0 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( 0 · 𝐴 ) ∈ ℝ )
3 1 2 mpan ⊢ ( 𝐴 ∈ ℝ → ( 0 · 𝐴 ) ∈ ℝ )
4 ax-rrecex ⊢ ( ( ( 0 · 𝐴 ) ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) → ∃ 𝑦 ∈ ℝ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 )
5 3 4 sylan ⊢ ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) → ∃ 𝑦 ∈ ℝ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 )
6 5 adantr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → ∃ 𝑦 ∈ ℝ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 )
7 00id ⊢ ( 0 + 0 ) = 0
8 7 oveq2i ⊢ ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · ( 0 + 0 ) ) = ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 )
9 8 eqcomi ⊢ ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) = ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · ( 0 + 0 ) )
10 simprl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → 𝑦 ∈ ℝ )
11 10 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → 𝑦 ∈ ℂ )
12 simplll ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → 𝐴 ∈ ℝ )
13 12 recnd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → 𝐴 ∈ ℂ )
14 11 13 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( 𝑦 · 𝐴 ) ∈ ℂ )
15 simplr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → 𝐵 ∈ ℂ )
16 0cn ⊢ 0 ∈ ℂ
17 mul32 ⊢ ( ( ( 𝑦 · 𝐴 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) = ( ( ( 𝑦 · 𝐴 ) · 0 ) · 𝐵 ) )
18 16 17 mp3an3 ⊢ ( ( ( 𝑦 · 𝐴 ) ∈ ℂ ∧ 𝐵 ∈ ℂ ) → ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) = ( ( ( 𝑦 · 𝐴 ) · 0 ) · 𝐵 ) )
19 14 15 18 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) = ( ( ( 𝑦 · 𝐴 ) · 0 ) · 𝐵 ) )
20 mul31 ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐴 ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( 𝑦 · 𝐴 ) · 0 ) = ( ( 0 · 𝐴 ) · 𝑦 ) )
21 16 20 mp3an3 ⊢ ( ( 𝑦 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( ( 𝑦 · 𝐴 ) · 0 ) = ( ( 0 · 𝐴 ) · 𝑦 ) )
22 11 13 21 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( ( 𝑦 · 𝐴 ) · 0 ) = ( ( 0 · 𝐴 ) · 𝑦 ) )
23 simprr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( ( 0 · 𝐴 ) · 𝑦 ) = 1 )
24 22 23 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( ( 𝑦 · 𝐴 ) · 0 ) = 1 )
25 24 oveq1d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( ( ( 𝑦 · 𝐴 ) · 0 ) · 𝐵 ) = ( 1 · 𝐵 ) )
26 mullid ⊢ ( 𝐵 ∈ ℂ → ( 1 · 𝐵 ) = 𝐵 )
27 26 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( 1 · 𝐵 ) = 𝐵 )
28 25 27 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( ( ( 𝑦 · 𝐴 ) · 0 ) · 𝐵 ) = 𝐵 )
29 19 28 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) = 𝐵 )
30 14 15 mulcld ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( ( 𝑦 · 𝐴 ) · 𝐵 ) ∈ ℂ )
31 adddi ⊢ ( ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) ∈ ℂ ∧ 0 ∈ ℂ ∧ 0 ∈ ℂ ) → ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · ( 0 + 0 ) ) = ( ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) + ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) ) )
32 16 16 31 mp3an23 ⊢ ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) ∈ ℂ → ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · ( 0 + 0 ) ) = ( ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) + ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) ) )
33 30 32 syl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · ( 0 + 0 ) ) = ( ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) + ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) ) )
34 29 29 oveq12d ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) + ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · 0 ) ) = ( 𝐵 + 𝐵 ) )
35 33 34 eqtrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → ( ( ( 𝑦 · 𝐴 ) · 𝐵 ) · ( 0 + 0 ) ) = ( 𝐵 + 𝐵 ) )
36 9 29 35 3eqtr3a ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) ∧ ( 𝑦 ∈ ℝ ∧ ( ( 0 · 𝐴 ) · 𝑦 ) = 1 ) ) → 𝐵 = ( 𝐵 + 𝐵 ) )
37 6 36 rexlimddv ⊢ ( ( ( 𝐴 ∈ ℝ ∧ ( 0 · 𝐴 ) ≠ 0 ) ∧ 𝐵 ∈ ℂ ) → 𝐵 = ( 𝐵 + 𝐵 ) )