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 x. _i ) = ( _i x. 1 )

Proof

Step Hyp Ref Expression
1 ax-icn 
 |-  _i e. CC
2 1 1 mulcli 
 |-  ( _i x. _i ) e. CC
3 2 2 1 mulassi 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. _i ) = ( ( _i x. _i ) x. ( ( _i x. _i ) x. _i ) )
4 1 2 mulcli 
 |-  ( _i x. ( _i x. _i ) ) e. CC
5 1 1 4 mulassi 
 |-  ( ( _i x. _i ) x. ( _i x. ( _i x. _i ) ) ) = ( _i x. ( _i x. ( _i x. ( _i x. _i ) ) ) )
6 1 1 1 mulassi 
 |-  ( ( _i x. _i ) x. _i ) = ( _i x. ( _i x. _i ) )
7 6 oveq2i 
 |-  ( ( _i x. _i ) x. ( ( _i x. _i ) x. _i ) ) = ( ( _i x. _i ) x. ( _i x. ( _i x. _i ) ) )
8 1 1 2 mulassi 
 |-  ( ( _i x. _i ) x. ( _i x. _i ) ) = ( _i x. ( _i x. ( _i x. _i ) ) )
9 8 oveq2i 
 |-  ( _i x. ( ( _i x. _i ) x. ( _i x. _i ) ) ) = ( _i x. ( _i x. ( _i x. ( _i x. _i ) ) ) )
10 5 7 9 3eqtr4i 
 |-  ( ( _i x. _i ) x. ( ( _i x. _i ) x. _i ) ) = ( _i x. ( ( _i x. _i ) x. ( _i x. _i ) ) )
11 3 10 eqtri 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. _i ) = ( _i x. ( ( _i x. _i ) x. ( _i x. _i ) ) )
12 rei4 
 |-  ( ( _i x. _i ) x. ( _i x. _i ) ) = 1
13 12 oveq1i 
 |-  ( ( ( _i x. _i ) x. ( _i x. _i ) ) x. _i ) = ( 1 x. _i )
14 12 oveq2i 
 |-  ( _i x. ( ( _i x. _i ) x. ( _i x. _i ) ) ) = ( _i x. 1 )
15 11 13 14 3eqtr3i 
 |-  ( 1 x. _i ) = ( _i x. 1 )