Theorem mulrid

Description: The number 1 is an identity element for multiplication. Based on ideas by Eric Schmidt. (Contributed by Scott Fenton, 3-Jan-2013)

	Ref	Expression
Assertion	mulrid	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		cnre	⊢ ( 𝐴 ∈ ℂ → ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
2		recn	⊢ ( 𝑥 ∈ ℝ → 𝑥 ∈ ℂ )
3		ax-icn	⊢ i ∈ ℂ
4		recn	⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℂ )
5		mulcl	⊢ ( ( i ∈ ℂ ∧ 𝑦 ∈ ℂ ) → ( i · 𝑦 ) ∈ ℂ )
6	3 4 5	sylancr	⊢ ( 𝑦 ∈ ℝ → ( i · 𝑦 ) ∈ ℂ )
7		ax-1cn	⊢ 1 ∈ ℂ
8		adddir	⊢ ( ( 𝑥 ∈ ℂ ∧ ( i · 𝑦 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑥 + ( i · 𝑦 ) ) · 1 ) = ( ( 𝑥 · 1 ) + ( ( i · 𝑦 ) · 1 ) ) )
9	7 8	mp3an3	⊢ ( ( 𝑥 ∈ ℂ ∧ ( i · 𝑦 ) ∈ ℂ ) → ( ( 𝑥 + ( i · 𝑦 ) ) · 1 ) = ( ( 𝑥 · 1 ) + ( ( i · 𝑦 ) · 1 ) ) )
10	2 6 9	syl2an	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( i · 𝑦 ) ) · 1 ) = ( ( 𝑥 · 1 ) + ( ( i · 𝑦 ) · 1 ) ) )
11		ax-1rid	⊢ ( 𝑥 ∈ ℝ → ( 𝑥 · 1 ) = 𝑥 )
12		mulass	⊢ ( ( i ∈ ℂ ∧ 𝑦 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( i · 𝑦 ) · 1 ) = ( i · ( 𝑦 · 1 ) ) )
13	3 7 12	mp3an13	⊢ ( 𝑦 ∈ ℂ → ( ( i · 𝑦 ) · 1 ) = ( i · ( 𝑦 · 1 ) ) )
14	4 13	syl	⊢ ( 𝑦 ∈ ℝ → ( ( i · 𝑦 ) · 1 ) = ( i · ( 𝑦 · 1 ) ) )
15		ax-1rid	⊢ ( 𝑦 ∈ ℝ → ( 𝑦 · 1 ) = 𝑦 )
16	15	oveq2d	⊢ ( 𝑦 ∈ ℝ → ( i · ( 𝑦 · 1 ) ) = ( i · 𝑦 ) )
17	14 16	eqtrd	⊢ ( 𝑦 ∈ ℝ → ( ( i · 𝑦 ) · 1 ) = ( i · 𝑦 ) )
18	11 17	oveqan12d	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 · 1 ) + ( ( i · 𝑦 ) · 1 ) ) = ( 𝑥 + ( i · 𝑦 ) ) )
19	10 18	eqtrd	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( ( 𝑥 + ( i · 𝑦 ) ) · 1 ) = ( 𝑥 + ( i · 𝑦 ) ) )
20		oveq1	⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 𝐴 · 1 ) = ( ( 𝑥 + ( i · 𝑦 ) ) · 1 ) )
21		id	⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) )
22	20 21	eqeq12d	⊢ ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( ( 𝐴 · 1 ) = 𝐴 ↔ ( ( 𝑥 + ( i · 𝑦 ) ) · 1 ) = ( 𝑥 + ( i · 𝑦 ) ) ) )
23	19 22	syl5ibrcom	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ) → ( 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 𝐴 · 1 ) = 𝐴 ) )
24	23	rexlimivv	⊢ ( ∃ 𝑥 ∈ ℝ ∃ 𝑦 ∈ ℝ 𝐴 = ( 𝑥 + ( i · 𝑦 ) ) → ( 𝐴 · 1 ) = 𝐴 )
25	1 24	syl	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · 1 ) = 𝐴 )