remulinvcom

Description: A left multiplicative inverse is a right multiplicative inverse. Proven without ax-mulcom . (Contributed by SN, 5-Feb-2024)

	Ref	Expression
Hypotheses	remulinvcom.1	$⊢ φ \to A \in ℝ$
	remulinvcom.2	$⊢ φ \to B \in ℝ$
	remulinvcom.3	$⊢ φ \to A B = 1$
Assertion	remulinvcom	$⊢ φ \to B A = 1$

Proof

Step	Hyp	Ref	Expression
1		remulinvcom.1	$⊢ φ \to A \in ℝ$
2		remulinvcom.2	$⊢ φ \to B \in ℝ$
3		remulinvcom.3	$⊢ φ \to A B = 1$
4		ax-1ne0	$⊢ 1 \neq 0$
5	4	a1i	$⊢ φ \to 1 \neq 0$
6	3 5	eqnetrd	$⊢ φ \to A B \neq 0$
7		simpr	$⊢ (φ \land B = 0) \to B = 0$
8	7	oveq2d	$⊢ (φ \land B = 0) \to A B = A \cdot 0$
9	1	adantr	$⊢ (φ \land B = 0) \to A \in ℝ$
10		remul01	$⊢ A \in ℝ \to A \cdot 0 = 0$
11	9 10	syl	$⊢ (φ \land B = 0) \to A \cdot 0 = 0$
12	8 11	eqtrd	$⊢ (φ \land B = 0) \to A B = 0$
13	6 12	mteqand	$⊢ φ \to B \neq 0$
14		ax-rrecex	$⊢ (B \in ℝ \land B \neq 0) \to \exists x \in ℝ B x = 1$
15	2 13 14	syl2anc	$⊢ φ \to \exists x \in ℝ B x = 1$
16		simprl	$⊢ (φ \land (x \in ℝ \land B x = 1)) \to x \in ℝ$
17		simprr	$⊢ (φ \land (x \in ℝ \land B x = 1)) \to B x = 1$
18	4	a1i	$⊢ (φ \land (x \in ℝ \land B x = 1)) \to 1 \neq 0$
19	17 18	eqnetrd	$⊢ (φ \land (x \in ℝ \land B x = 1)) \to B x \neq 0$
20		simpr	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land x = 0) \to x = 0$
21	20	oveq2d	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land x = 0) \to B x = B \cdot 0$
22	2	ad2antrr	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land x = 0) \to B \in ℝ$
23		remul01	$⊢ B \in ℝ \to B \cdot 0 = 0$
24	22 23	syl	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land x = 0) \to B \cdot 0 = 0$
25	21 24	eqtrd	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land x = 0) \to B x = 0$
26	19 25	mteqand	$⊢ (φ \land (x \in ℝ \land B x = 1)) \to x \neq 0$
27		ax-rrecex	$⊢ (x \in ℝ \land x \neq 0) \to \exists y \in ℝ x y = 1$
28	16 26 27	syl2anc	$⊢ (φ \land (x \in ℝ \land B x = 1)) \to \exists y \in ℝ x y = 1$
29		simplrr	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to B x = 1$
30	29	oveq2d	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A B x = A \cdot 1$
31	30	oveq1d	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A B x y = A \cdot 1 y$
32	1	ad2antrr	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A \in ℝ$
33	2	ad2antrr	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to B \in ℝ$
34	32 33	remulcld	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A B \in ℝ$
35	34	recnd	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A B \in ℂ$
36		simplrl	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to x \in ℝ$
37	36	recnd	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to x \in ℂ$
38		simprl	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to y \in ℝ$
39	38	recnd	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to y \in ℂ$
40	35 37 39	mulassd	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A B x y = A B x y$
41	32	recnd	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A \in ℂ$
42	33	recnd	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to B \in ℂ$
43	41 42 37	mulassd	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A B x = A B x$
44	43	oveq1d	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A B x y = A B x y$
45	3	ad2antrr	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A B = 1$
46		simprr	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to x y = 1$
47	45 46	oveq12d	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A B x y = 1 \cdot 1$
48		1t1e1ALT	$⊢ 1 \cdot 1 = 1$
49	47 48	syl6eq	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A B x y = 1$
50	40 44 49	3eqtr3d	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A B x y = 1$
51		ax-1rid	$⊢ A \in ℝ \to A \cdot 1 = A$
52	32 51	syl	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A \cdot 1 = A$
53	52	oveq1d	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A \cdot 1 y = A y$
54	31 50 53	3eqtr3rd	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A y = 1$
55	54 46	eqtr4d	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A y = x y$
56	4	a1i	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to 1 \neq 0$
57	46 56	eqnetrd	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to x y \neq 0$
58		simpr	$⊢ (((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \land y = 0) \to y = 0$
59	58	oveq2d	$⊢ (((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \land y = 0) \to x y = x \cdot 0$
60	36	adantr	$⊢ (((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \land y = 0) \to x \in ℝ$
61		remul01	$⊢ x \in ℝ \to x \cdot 0 = 0$
62	60 61	syl	$⊢ (((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \land y = 0) \to x \cdot 0 = 0$
63	59 62	eqtrd	$⊢ (((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \land y = 0) \to x y = 0$
64	57 63	mteqand	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to y \neq 0$
65	32 36 38 64	remulcan2d	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to (A y = x y \leftrightarrow A = x)$
66	55 65	mpbid	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to A = x$
67		simpr	$⊢ (((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \land A = x) \to A = x$
68	67	oveq2d	$⊢ (((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \land A = x) \to B A = B x$
69	17	ad2antrr	$⊢ (((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \land A = x) \to B x = 1$
70	68 69	eqtrd	$⊢ (((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \land A = x) \to B A = 1$
71	66 70	mpdan	$⊢ ((φ \land (x \in ℝ \land B x = 1)) \land (y \in ℝ \land x y = 1)) \to B A = 1$
72	28 71	rexlimddv	$⊢ (φ \land (x \in ℝ \land B x = 1)) \to B A = 1$
73	15 72	rexlimddv	$⊢ φ \to B A = 1$

Metamath Proof Explorer

Theorem remulinvcom

Proof