Theorem smup1

Description: Rewrite smupp1 using only smul instead of the internal recursive function P . (Contributed by Mario Carneiro, 20-Sep-2016)

	Ref	Expression
Hypotheses	smup1.a	|- ( ph -> A C_ NN0 )
	smup1.b	|- ( ph -> B C_ NN0 )
	smup1.n	|- ( ph -> N e. NN0 )
Assertion	smup1	|- ( ph -> ( ( A i^i ( 0 ..^ ( N + 1 ) ) ) smul B ) = ( ( ( A i^i ( 0 ..^ N ) ) smul B ) sadd { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) } ) )

Proof

Step	Hyp	Ref	Expression
1		smup1.a	|- ( ph -> A C_ NN0 )
2		smup1.b	|- ( ph -> B C_ NN0 )
3		smup1.n	|- ( ph -> N e. NN0 )
4		eqid	|- seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) = seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
5	1 2 4 3	smupp1	|- ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( N + 1 ) ) = ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N ) sadd { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) } ) )
6		peano2nn0	|- ( N e. NN0 -> ( N + 1 ) e. NN0 )
7	3 6	syl	|- ( ph -> ( N + 1 ) e. NN0 )
8	1 2 4 7	smupval	|- ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` ( N + 1 ) ) = ( ( A i^i ( 0 ..^ ( N + 1 ) ) ) smul B ) )
9	1 2 4 3	smupval	|- ( ph -> ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N ) = ( ( A i^i ( 0 ..^ N ) ) smul B ) )
10	9	oveq1d	|- ( ph -> ( ( seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. B ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) ) ` N ) sadd { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) } ) = ( ( ( A i^i ( 0 ..^ N ) ) smul B ) sadd { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) } ) )
11	5 8 10	3eqtr3d	|- ( ph -> ( ( A i^i ( 0 ..^ ( N + 1 ) ) ) smul B ) = ( ( ( A i^i ( 0 ..^ N ) ) smul B ) sadd { n e. NN0 | ( N e. A /\ ( n - N ) e. B ) } ) )