remulid2

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

		Ref	Expression
	Assertion	remulid2	$⊢ A \in ℝ \to 1 A = A$

Proof

Step	Hyp	Ref	Expression
1		df-ne	$⊢ A \neq 0 \leftrightarrow \neg A = 0$
2		ax-rrecex	$⊢ (A \in ℝ \land A \neq 0) \to \exists x \in ℝ A x = 1$
3		simpll	$⊢ ((A \in ℝ \land A \neq 0) \land (x \in ℝ \land A x = 1)) \to A \in ℝ$
4	3	recnd	$⊢ ((A \in ℝ \land A \neq 0) \land (x \in ℝ \land A x = 1)) \to A \in ℂ$
5		simprl	$⊢ ((A \in ℝ \land A \neq 0) \land (x \in ℝ \land A x = 1)) \to x \in ℝ$
6	5	recnd	$⊢ ((A \in ℝ \land A \neq 0) \land (x \in ℝ \land A x = 1)) \to x \in ℂ$
7	4 6 4	mulassd	$⊢ ((A \in ℝ \land A \neq 0) \land (x \in ℝ \land A x = 1)) \to A x A = A x A$
8		simprr	$⊢ ((A \in ℝ \land A \neq 0) \land (x \in ℝ \land A x = 1)) \to A x = 1$
9	8	oveq1d	$⊢ ((A \in ℝ \land A \neq 0) \land (x \in ℝ \land A x = 1)) \to A x A = 1 A$
10	3 5 8	remulinvcom	$⊢ ((A \in ℝ \land A \neq 0) \land (x \in ℝ \land A x = 1)) \to x A = 1$
11	10	oveq2d	$⊢ ((A \in ℝ \land A \neq 0) \land (x \in ℝ \land A x = 1)) \to A x A = A \cdot 1$
12		ax-1rid	$⊢ A \in ℝ \to A \cdot 1 = A$
13	3 12	syl	$⊢ ((A \in ℝ \land A \neq 0) \land (x \in ℝ \land A x = 1)) \to A \cdot 1 = A$
14	11 13	eqtrd	$⊢ ((A \in ℝ \land A \neq 0) \land (x \in ℝ \land A x = 1)) \to A x A = A$
15	7 9 14	3eqtr3d	$⊢ ((A \in ℝ \land A \neq 0) \land (x \in ℝ \land A x = 1)) \to 1 A = A$
16	2 15	rexlimddv	$⊢ (A \in ℝ \land A \neq 0) \to 1 A = A$
17	16	ex	$⊢ A \in ℝ \to (A \neq 0 \to 1 A = A)$
18	1 17	syl5bir	$⊢ A \in ℝ \to (\neg A = 0 \to 1 A = A)$
19		1re	$⊢ 1 \in ℝ$
20		remul01	$⊢ 1 \in ℝ \to 1 \cdot 0 = 0$
21	19 20	mp1i	$⊢ A = 0 \to 1 \cdot 0 = 0$
22		oveq2	$⊢ A = 0 \to 1 A = 1 \cdot 0$
23		id	$⊢ A = 0 \to A = 0$
24	21 22 23	3eqtr4d	$⊢ A = 0 \to 1 A = A$
25	18 24	pm2.61d2	$⊢ A \in ℝ \to 1 A = A$

Metamath Proof Explorer

Theorem remulid2

Proof