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 ⊢A∈ℝ∧0⋅A≠0∧B∈ℂ→B=B+B

Proof

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