Metamath Proof Explorer


Theorem sn-mulid2

Description: mulid2 without ax-mulcom . (Contributed by SN, 27-May-2024)

Ref Expression
Assertion sn-mulid2 A 1 A = A

Proof

Step Hyp Ref Expression
1 cnre A x y A = x + i y
2 1cnd x y 1
3 recn x x
4 3 adantr x y x
5 ax-icn i
6 5 a1i x y i
7 recn y y
8 7 adantl x y y
9 6 8 mulcld x y i y
10 2 4 9 adddid x y 1 x + i y = 1 x + 1 i y
11 remulid2 x 1 x = x
12 11 adantr x y 1 x = x
13 2 6 8 mulassd x y 1 i y = 1 i y
14 sn-1ticom 1 i = i 1
15 14 oveq1i 1 i y = i 1 y
16 15 a1i x y 1 i y = i 1 y
17 6 2 8 mulassd x y i 1 y = i 1 y
18 remulid2 y 1 y = y
19 18 adantl x y 1 y = y
20 19 oveq2d x y i 1 y = i y
21 16 17 20 3eqtrd x y 1 i y = i y
22 13 21 eqtr3d x y 1 i y = i y
23 12 22 oveq12d x y 1 x + 1 i y = x + i y
24 10 23 eqtrd x y 1 x + i y = x + i y
25 oveq2 A = x + i y 1 A = 1 x + i y
26 id A = x + i y A = x + i y
27 25 26 eqeq12d A = x + i y 1 A = A 1 x + i y = x + i y
28 24 27 syl5ibrcom x y A = x + i y 1 A = A
29 28 rexlimivv x y A = x + i y 1 A = A
30 1 29 syl A 1 A = A