Theorem smueq

Description: Any element of a sequence multiplication only depends on the values of the argument sequences up to and including that point. (Contributed by Mario Carneiro, 20-Sep-2016)

	Ref	Expression
Hypotheses	smueq.a	|- ( ph -> A C_ NN0 )
	smueq.b	|- ( ph -> B C_ NN0 )
	smueq.n	|- ( ph -> N e. NN0 )
Assertion	smueq	|- ( ph -> ( ( A smul B ) i^i ( 0 ..^ N ) ) = ( ( ( A i^i ( 0 ..^ N ) ) smul ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )

Proof

Step	Hyp	Ref	Expression
1		smueq.a	|- ( ph -> A C_ NN0 )
2		smueq.b	|- ( ph -> B C_ NN0 )
3		smueq.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		eqid	|- seq 0 ( ( p e. ~P NN0 , m e. NN0 |-> ( p sadd { n e. NN0 | ( m e. A /\ ( n - m ) e. ( B i^i ( 0 ..^ N ) ) ) } ) ) , ( 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 i^i ( 0 ..^ N ) ) ) } ) ) , ( n e. NN0 |-> if ( n = 0 , (/) , ( n - 1 ) ) ) )
6	1 2 3 4 5	smueqlem	|- ( ph -> ( ( A smul B ) i^i ( 0 ..^ N ) ) = ( ( ( A i^i ( 0 ..^ N ) ) smul ( B i^i ( 0 ..^ N ) ) ) i^i ( 0 ..^ N ) ) )