Metamath Proof Explorer


Theorem sn-1ticom

Description: Lemma for sn-mulid2 and it1ei . (Contributed by SN, 27-May-2024)

Ref Expression
Assertion sn-1ticom 1 i = i 1

Proof

Step Hyp Ref Expression
1 ax-icn i
2 1 1 mulcli i i
3 2 2 1 mulassi i i i i i = i i i i i
4 1 2 mulcli i i i
5 1 1 4 mulassi i i i i i = i i i i i
6 1 1 1 mulassi i i i = i i i
7 6 oveq2i i i i i i = i i i i i
8 1 1 2 mulassi i i i i = i i i i
9 8 oveq2i i i i i i = i i i i i
10 5 7 9 3eqtr4i i i i i i = i i i i i
11 3 10 eqtri i i i i i = i i i i i
12 rei4 i i i i = 1
13 12 oveq1i i i i i i = 1 i
14 12 oveq2i i i i i i = i 1
15 11 13 14 3eqtr3i 1 i = i 1