This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sn-1ticom

Description: Lemma for sn-mullid and sn-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 )