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

Metamath Proof Explorer

Theorem remullid

Description: Commuted version of ax-1rid without ax-mulcom . (Contributed by SN, 5-Feb-2024)

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

Proof

Step Hyp Ref Expression
1 df-ne ⊢ ( 𝐴 ≠ 0 ↔ ¬ 𝐴 = 0 )
2 ax-rrecex ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ∃ 𝑥 ∈ ℝ ( 𝐴 · 𝑥 ) = 1 )
3 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) → 𝐴 ∈ ℝ )
4 3 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) → 𝐴 ∈ ℂ )
5 simprl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℝ )
6 5 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) → 𝑥 ∈ ℂ )
7 4 6 4 mulassd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 𝑥 ) · 𝐴 ) = ( 𝐴 · ( 𝑥 · 𝐴 ) ) )
8 simprr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) → ( 𝐴 · 𝑥 ) = 1 )
9 8 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) → ( ( 𝐴 · 𝑥 ) · 𝐴 ) = ( 1 · 𝐴 ) )
10 3 5 8 remulinvcom ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) → ( 𝑥 · 𝐴 ) = 1 )
11 10 oveq2d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) → ( 𝐴 · ( 𝑥 · 𝐴 ) ) = ( 𝐴 · 1 ) )
12 ax-1rid ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 · 1 ) = 𝐴 )
13 3 12 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) → ( 𝐴 · 1 ) = 𝐴 )
14 11 13 eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) → ( 𝐴 · ( 𝑥 · 𝐴 ) ) = 𝐴 )
15 7 9 14 3eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) ∧ ( 𝑥 ∈ ℝ ∧ ( 𝐴 · 𝑥 ) = 1 ) ) → ( 1 · 𝐴 ) = 𝐴 )
16 2 15 rexlimddv ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝐴 ≠ 0 ) → ( 1 · 𝐴 ) = 𝐴 )
17 16 ex ⊢ ( 𝐴 ∈ ℝ → ( 𝐴 ≠ 0 → ( 1 · 𝐴 ) = 𝐴 ) )
18 1 17 biimtrrid ⊢ ( 𝐴 ∈ ℝ → ( ¬ 𝐴 = 0 → ( 1 · 𝐴 ) = 𝐴 ) )
19 1re ⊢ 1 ∈ ℝ
20 remul01 ⊢ ( 1 ∈ ℝ → ( 1 · 0 ) = 0 )
21 19 20 mp1i ⊢ ( 𝐴 = 0 → ( 1 · 0 ) = 0 )
22 oveq2 ⊢ ( 𝐴 = 0 → ( 1 · 𝐴 ) = ( 1 · 0 ) )
23 id ⊢ ( 𝐴 = 0 → 𝐴 = 0 )
24 21 22 23 3eqtr4d ⊢ ( 𝐴 = 0 → ( 1 · 𝐴 ) = 𝐴 )
25 18 24 pm2.61d2 ⊢ ( 𝐴 ∈ ℝ → ( 1 · 𝐴 ) = 𝐴 )