Metamath Proof Explorer

Theorem 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 ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
remulinvcom.2 ⊢ ( 𝜑 → 𝐵 ∈ ℝ )
remulinvcom.3 ⊢ ( 𝜑 → ( 𝐴 · 𝐵 ) = 1 )
Assertion remulinvcom ( 𝜑 → ( 𝐵 · 𝐴 ) = 1 )

Proof

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