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 < 𝑁 , ( 𝑆 ‘ 𝑁 ) , ( 𝐼 ‘ ( 𝑆 ‘ - 𝑁 ) ) ) ) )