Metamath Proof Explorer


Theorem remulid2

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

Ref Expression
Assertion remulid2 A1A=A

Proof

Step Hyp Ref Expression
1 df-ne A0¬A=0
2 ax-rrecex AA0xAx=1
3 simpll AA0xAx=1A
4 3 recnd AA0xAx=1A
5 simprl AA0xAx=1x
6 5 recnd AA0xAx=1x
7 4 6 4 mulassd AA0xAx=1AxA=AxA
8 simprr AA0xAx=1Ax=1
9 8 oveq1d AA0xAx=1AxA=1A
10 3 5 8 remulinvcom AA0xAx=1xA=1
11 10 oveq2d AA0xAx=1AxA=A1
12 ax-1rid AA1=A
13 3 12 syl AA0xAx=1A1=A
14 11 13 eqtrd AA0xAx=1AxA=A
15 7 9 14 3eqtr3d AA0xAx=11A=A
16 2 15 rexlimddv AA01A=A
17 16 ex AA01A=A
18 1 17 syl5bir A¬A=01A=A
19 1re 1
20 remul01 110=0
21 19 20 mp1i A=010=0
22 oveq2 A=01A=10
23 id A=0A=0
24 21 22 23 3eqtr4d A=01A=A
25 18 24 pm2.61d2 A1A=A