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

Metamath Proof Explorer

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 mulrid , 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 eqtrid ⊢ ( 𝑥 ∈ 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 imbitrrid ⊢ ( 𝑦 = 0R → ( 𝑥 ∈ R → ( ⟨ 𝑥 , 𝑦 ⟩ · 1 ) = ⟨ 𝑥 , 𝑦 ⟩ ) )
19 18 impcom ⊢ ( ( 𝑥 ∈ R ∧ 𝑦 = 0R ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 1 ) = ⟨ 𝑥 , 𝑦 ⟩ )
20 5 19 sylan2 ⊢ ( ( 𝑥 ∈ R ∧ 𝑦 ∈ { 0R } ) → ( ⟨ 𝑥 , 𝑦 ⟩ · 1 ) = ⟨ 𝑥 , 𝑦 ⟩ )
21 1 4 20 optocl ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )