Theorem ax1rid

Description: 1 is an identity element for real multiplication. Axiom 14 of 22 for real and complex numbers, derived from ZF set theory. Weakened from the original axiom in the form of statement in mulid1 , based on ideas by Eric Schmidt. This construction-dependent theorem should not be referenced directly; instead, use ax-1rid . (Contributed by Scott Fenton, 3-Jan-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	ax1rid	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		df-r	⊢ ℝ = ( R × { 0R } )
2		oveq1	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 → ( ⟨ 𝑥 , 𝑦 ⟩ · 1 ) = ( 𝐴 · 1 ) )
3		id	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 → ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 )
4	2 3	eqeq12d	⊢ ( ⟨ 𝑥 , 𝑦 ⟩ = 𝐴 → ( ( ⟨ 𝑥 , 𝑦 ⟩ · 1 ) = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( 𝐴 · 1 ) = 𝐴 ) )
5		elsni	⊢ ( 𝑦 ∈ { 0R } → 𝑦 = 0R )
6		df-1	⊢ 1 = ⟨ 1R , 0R ⟩
7	6	oveq2i	⊢ ( ⟨ 𝑥 , 0R ⟩ · 1 ) = ( ⟨ 𝑥 , 0R ⟩ · ⟨ 1R , 0R ⟩ )
8		1sr	⊢ 1R ∈ R
9		mulresr	⊢ ( ( 𝑥 ∈ R ∧ 1R ∈ R ) → ( ⟨ 𝑥 , 0R ⟩ · ⟨ 1R , 0R ⟩ ) = ⟨ ( 𝑥 ·R 1R ) , 0R ⟩ )
10	8 9	mpan2	⊢ ( 𝑥 ∈ R → ( ⟨ 𝑥 , 0R ⟩ · ⟨ 1R , 0R ⟩ ) = ⟨ ( 𝑥 ·R 1R ) , 0R ⟩ )
11		1idsr	⊢ ( 𝑥 ∈ R → ( 𝑥 ·R 1R ) = 𝑥 )
12	11	opeq1d	⊢ ( 𝑥 ∈ R → ⟨ ( 𝑥 ·R 1R ) , 0R ⟩ = ⟨ 𝑥 , 0R ⟩ )
13	10 12	eqtrd	⊢ ( 𝑥 ∈ R → ( ⟨ 𝑥 , 0R ⟩ · ⟨ 1R , 0R ⟩ ) = ⟨ 𝑥 , 0R ⟩ )
14	7 13	syl5eq	⊢ ( 𝑥 ∈ R → ( ⟨ 𝑥 , 0R ⟩ · 1 ) = ⟨ 𝑥 , 0R ⟩ )
15		opeq2	⊢ ( 𝑦 = 0R → ⟨ 𝑥 , 𝑦 ⟩ = ⟨ 𝑥 , 0R ⟩ )
16	15	oveq1d	⊢ ( 𝑦 = 0R → ( ⟨ 𝑥 , 𝑦 ⟩ · 1 ) = ( ⟨ 𝑥 , 0R ⟩ · 1 ) )
17	16 15	eqeq12d	⊢ ( 𝑦 = 0R → ( ( ⟨ 𝑥 , 𝑦 ⟩ · 1 ) = ⟨ 𝑥 , 𝑦 ⟩ ↔ ( ⟨ 𝑥 , 0R ⟩ · 1 ) = ⟨ 𝑥 , 0R ⟩ ) )
18	14 17	syl5ibr	⊢ ( 𝑦 = 0R → ( 𝑥 ∈ R → ( ⟨ 𝑥 , 𝑦 ⟩ · 1 ) = ⟨ 𝑥 , 𝑦 ⟩ ) )
19	18	impcom	⊢ ( ( 𝑥 ∈ R ∧ 𝑦 = 0R ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 1 ) = ⟨ 𝑥 , 𝑦 ⟩ )
20	5 19	sylan2	⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ { 0R } ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 1 ) = ⟨ 𝑥 , 𝑦 ⟩ )
21	1 4 20	optocl	⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )