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 
|- ( ph -> A e. RR )
remulinvcom.2 
|- ( ph -> B e. RR )
remulinvcom.3 
|- ( ph -> ( A x. B ) = 1 )
Assertion remulinvcom 
|- ( ph -> ( B x. A ) = 1 )

Proof

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