Metamath Proof Explorer

Theorem remulid2

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

Ref Expression
Assertion remulid2 
|- ( A e. RR -> ( 1 x. A ) = A )

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( A =/= 0 <-> -. A = 0 )
2 ax-rrecex 
 |-  ( ( A e. RR /\ A =/= 0 ) -> E. x e. RR ( A x. x ) = 1 )
3 simpll 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ ( x e. RR /\ ( A x. x ) = 1 ) ) -> A e. RR )
4 3 recnd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ ( x e. RR /\ ( A x. x ) = 1 ) ) -> A e. CC )
5 simprl 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ ( x e. RR /\ ( A x. x ) = 1 ) ) -> x e. RR )
6 5 recnd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ ( x e. RR /\ ( A x. x ) = 1 ) ) -> x e. CC )
7 4 6 4 mulassd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ ( x e. RR /\ ( A x. x ) = 1 ) ) -> ( ( A x. x ) x. A ) = ( A x. ( x x. A ) ) )
8 simprr 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ ( x e. RR /\ ( A x. x ) = 1 ) ) -> ( A x. x ) = 1 )
9 8 oveq1d 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ ( x e. RR /\ ( A x. x ) = 1 ) ) -> ( ( A x. x ) x. A ) = ( 1 x. A ) )
10 3 5 8 remulinvcom 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ ( x e. RR /\ ( A x. x ) = 1 ) ) -> ( x x. A ) = 1 )
11 10 oveq2d 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ ( x e. RR /\ ( A x. x ) = 1 ) ) -> ( A x. ( x x. A ) ) = ( A x. 1 ) )
12 ax-1rid 
 |-  ( A e. RR -> ( A x. 1 ) = A )
13 3 12 syl 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ ( x e. RR /\ ( A x. x ) = 1 ) ) -> ( A x. 1 ) = A )
14 11 13 eqtrd 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ ( x e. RR /\ ( A x. x ) = 1 ) ) -> ( A x. ( x x. A ) ) = A )
15 7 9 14 3eqtr3d 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ ( x e. RR /\ ( A x. x ) = 1 ) ) -> ( 1 x. A ) = A )
16 2 15 rexlimddv 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( 1 x. A ) = A )
17 16 ex 
 |-  ( A e. RR -> ( A =/= 0 -> ( 1 x. A ) = A ) )
18 1 17 syl5bir 
 |-  ( A e. RR -> ( -. A = 0 -> ( 1 x. A ) = A ) )
19 1re 
 |-  1 e. RR
20 remul01 
 |-  ( 1 e. RR -> ( 1 x. 0 ) = 0 )
21 19 20 mp1i 
 |-  ( A = 0 -> ( 1 x. 0 ) = 0 )
22 oveq2 
 |-  ( A = 0 -> ( 1 x. A ) = ( 1 x. 0 ) )
23 id 
 |-  ( A = 0 -> A = 0 )
24 21 22 23 3eqtr4d 
 |-  ( A = 0 -> ( 1 x. A ) = A )
25 18 24 pm2.61d2 
 |-  ( A e. RR -> ( 1 x. A ) = A )