Theorem remulid2

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

	Ref	Expression
Assertion	remulid2	⊢ ( 𝐴 ∈ ℝ → ( 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	syl5bir	⊢ ( 𝐴 ∈ ℝ → ( ¬ 𝐴 = 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 · 𝐴 ) = 𝐴 )