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

Metamath Proof Explorer

Theorem mulgval

Description: Value of the group multiple (exponentiation) operation. (Contributed by Mario Carneiro, 11-Dec-2014)

Ref Expression
Hypotheses mulgval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
mulgval.p ⊢ + = ( +g ‘ 𝐺 )
mulgval.o ⊢ 0 = ( 0g ‘ 𝐺 )
mulgval.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
mulgval.t ⊢ · = ( .g ‘ 𝐺 )
mulgval.s ⊢ 𝑆 = seq 1 ( + , ( ℕ × { 𝑋 } ) )
Assertion mulgval ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = if ( 𝑁 = 0 , 0 , if ( 0 < 𝑁 , ( 𝑆 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝑆 ‘ - 𝑁 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 mulgval.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
2 mulgval.p ⊢ + = ( +g ‘ 𝐺 )
3 mulgval.o ⊢ 0 = ( 0g ‘ 𝐺 )
4 mulgval.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
5 mulgval.t ⊢ · = ( .g ‘ 𝐺 )
6 mulgval.s ⊢ 𝑆 = seq 1 ( + , ( ℕ × { 𝑋 } ) )
7 simpl ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → 𝑛 = 𝑁 )
8 7 eqeq1d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( 𝑛 = 0 ↔ 𝑁 = 0 ) )
9 7 breq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( 0 < 𝑛 ↔ 0 < 𝑁 ) )
10 simpr ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → 𝑥 = 𝑋 )
11 10 sneqd ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → { 𝑥 } = { 𝑋 } )
12 11 xpeq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( ℕ × { 𝑥 } ) = ( ℕ × { 𝑋 } ) )
13 12 seqeq3d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → seq 1 ( + , ( ℕ × { 𝑥 } ) ) = seq 1 ( + , ( ℕ × { 𝑋 } ) ) )
14 13 6 eqtr4di ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → seq 1 ( + , ( ℕ × { 𝑥 } ) ) = 𝑆 )
15 14 7 fveq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) = ( 𝑆 ‘ 𝑁 ) )
16 7 negeqd ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → - 𝑛 = - 𝑁 )
17 14 16 fveq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) = ( 𝑆 ‘ - 𝑁 ) )
18 17 fveq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) = ( 𝐼 ‘ ( 𝑆 ‘ - 𝑁 ) ) )
19 9 15 18 ifbieq12d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) = if ( 0 < 𝑁 , ( 𝑆 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝑆 ‘ - 𝑁 ) ) ) )
20 8 19 ifbieq2d ⊢ ( ( 𝑛 = 𝑁 ∧ 𝑥 = 𝑋 ) → if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) = if ( 𝑁 = 0 , 0 , if ( 0 < 𝑁 , ( 𝑆 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝑆 ‘ - 𝑁 ) ) ) ) )
21 1 2 3 4 5 mulgfval ⊢ · = ( 𝑛 ∈ ℤ , 𝑥 ∈ 𝐵 ↦ if ( 𝑛 = 0 , 0 , if ( 0 < 𝑛 , ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ 𝑛 ) , ( 𝐼 ‘ ( seq 1 ( + , ( ℕ × { 𝑥 } ) ) ‘ - 𝑛 ) ) ) ) )
22 3 fvexi ⊢ 0 ∈ V
23 fvex ⊢ ( 𝑆 ‘ 𝑁 ) ∈ V
24 fvex ⊢ ( 𝐼 ‘ ( 𝑆 ‘ - 𝑁 ) ) ∈ V
25 23 24 ifex ⊢ if ( 0 < 𝑁 , ( 𝑆 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝑆 ‘ - 𝑁 ) ) ) ∈ V
26 22 25 ifex ⊢ if ( 𝑁 = 0 , 0 , if ( 0 < 𝑁 , ( 𝑆 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝑆 ‘ - 𝑁 ) ) ) ) ∈ V
27 20 21 26 ovmpoa ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑋 ∈ 𝐵 ) → ( 𝑁 · 𝑋 ) = if ( 𝑁 = 0 , 0 , if ( 0 < 𝑁 , ( 𝑆 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝑆 ‘ - 𝑁 ) ) ) ) )