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 ) ∧ 𝐵 ∈ ℂ ) → 𝐵 = ( 𝐵 + 𝐵 ) )