Metamath Proof Explorer

Theorem seqof2

Description: Distribute function operation through a sequence. Maps-to notation version of seqof . (Contributed by Mario Carneiro, 7-Jul-2017)

Ref Expression
Hypotheses seqof2.1 
|- ( ph -> A e. V )
seqof2.2 
|- ( ph -> N e. ( ZZ>= ` M ) )
seqof2.3 
|- ( ph -> ( M ... N ) C_ B )
seqof2.4 
|- ( ( ph /\ ( x e. B /\ z e. A ) ) -> X e. W )
Assertion seqof2 
|- ( ph -> ( seq M ( oF .+ , ( x e. B |-> ( z e. A |-> X ) ) ) ` N ) = ( z e. A |-> ( seq M ( .+ , ( x e. B |-> X ) ) ` N ) ) )

Proof

Step Hyp Ref Expression
1 seqof2.1 
 |-  ( ph -> A e. V )
2 seqof2.2 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
3 seqof2.3 
 |-  ( ph -> ( M ... N ) C_ B )
4 seqof2.4 
 |-  ( ( ph /\ ( x e. B /\ z e. A ) ) -> X e. W )
5 nfv 
 |-  F/ x ( ph /\ n e. ( M ... N ) )
6 nffvmpt1 
 |-  F/_ x ( ( x e. B |-> ( z e. A |-> X ) ) ` n )
7 nfcv 
 |-  F/_ x A
8 nffvmpt1 
 |-  F/_ x ( ( x e. B |-> X ) ` n )
9 7 8 nfmpt 
 |-  F/_ x ( z e. A |-> ( ( x e. B |-> X ) ` n ) )
10 6 9 nfeq 
 |-  F/ x ( ( x e. B |-> ( z e. A |-> X ) ) ` n ) = ( z e. A |-> ( ( x e. B |-> X ) ` n ) )
11 5 10 nfim 
 |-  F/ x ( ( ph /\ n e. ( M ... N ) ) -> ( ( x e. B |-> ( z e. A |-> X ) ) ` n ) = ( z e. A |-> ( ( x e. B |-> X ) ` n ) ) )
12 eleq1w 
 |-  ( x = n -> ( x e. ( M ... N ) <-> n e. ( M ... N ) ) )
13 12 anbi2d 
 |-  ( x = n -> ( ( ph /\ x e. ( M ... N ) ) <-> ( ph /\ n e. ( M ... N ) ) ) )
14 fveq2 
 |-  ( x = n -> ( ( x e. B |-> ( z e. A |-> X ) ) ` x ) = ( ( x e. B |-> ( z e. A |-> X ) ) ` n ) )
15 fveq2 
 |-  ( x = n -> ( ( x e. B |-> X ) ` x ) = ( ( x e. B |-> X ) ` n ) )
16 15 mpteq2dv 
 |-  ( x = n -> ( z e. A |-> ( ( x e. B |-> X ) ` x ) ) = ( z e. A |-> ( ( x e. B |-> X ) ` n ) ) )
17 14 16 eqeq12d 
 |-  ( x = n -> ( ( ( x e. B |-> ( z e. A |-> X ) ) ` x ) = ( z e. A |-> ( ( x e. B |-> X ) ` x ) ) <-> ( ( x e. B |-> ( z e. A |-> X ) ) ` n ) = ( z e. A |-> ( ( x e. B |-> X ) ` n ) ) ) )
18 13 17 imbi12d 
 |-  ( x = n -> ( ( ( ph /\ x e. ( M ... N ) ) -> ( ( x e. B |-> ( z e. A |-> X ) ) ` x ) = ( z e. A |-> ( ( x e. B |-> X ) ` x ) ) ) <-> ( ( ph /\ n e. ( M ... N ) ) -> ( ( x e. B |-> ( z e. A |-> X ) ) ` n ) = ( z e. A |-> ( ( x e. B |-> X ) ` n ) ) ) ) )
19 3 sselda 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> x e. B )
20 1 adantr 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> A e. V )
21 20 mptexd 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( z e. A |-> X ) e. _V )
22 eqid 
 |-  ( x e. B |-> ( z e. A |-> X ) ) = ( x e. B |-> ( z e. A |-> X ) )
23 22 fvmpt2 
 |-  ( ( x e. B /\ ( z e. A |-> X ) e. _V ) -> ( ( x e. B |-> ( z e. A |-> X ) ) ` x ) = ( z e. A |-> X ) )
24 19 21 23 syl2anc 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( ( x e. B |-> ( z e. A |-> X ) ) ` x ) = ( z e. A |-> X ) )
25 19 adantr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ z e. A ) -> x e. B )
26 simpll 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ z e. A ) -> ph )
27 simpr 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ z e. A ) -> z e. A )
28 26 25 27 4 syl12anc 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ z e. A ) -> X e. W )
29 eqid 
 |-  ( x e. B |-> X ) = ( x e. B |-> X )
30 29 fvmpt2 
 |-  ( ( x e. B /\ X e. W ) -> ( ( x e. B |-> X ) ` x ) = X )
31 25 28 30 syl2anc 
 |-  ( ( ( ph /\ x e. ( M ... N ) ) /\ z e. A ) -> ( ( x e. B |-> X ) ` x ) = X )
32 31 mpteq2dva 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( z e. A |-> ( ( x e. B |-> X ) ` x ) ) = ( z e. A |-> X ) )
33 24 32 eqtr4d 
 |-  ( ( ph /\ x e. ( M ... N ) ) -> ( ( x e. B |-> ( z e. A |-> X ) ) ` x ) = ( z e. A |-> ( ( x e. B |-> X ) ` x ) ) )
34 11 18 33 chvarfv 
 |-  ( ( ph /\ n e. ( M ... N ) ) -> ( ( x e. B |-> ( z e. A |-> X ) ) ` n ) = ( z e. A |-> ( ( x e. B |-> X ) ` n ) ) )
35 nfcv 
 |-  F/_ y ( ( x e. B |-> X ) ` n )
36 nfcsb1v 
 |-  F/_ z [_ y / z ]_ ( x e. B |-> X )
37 nfcv 
 |-  F/_ z n
38 36 37 nffv 
 |-  F/_ z ( [_ y / z ]_ ( x e. B |-> X ) ` n )
39 csbeq1a 
 |-  ( z = y -> ( x e. B |-> X ) = [_ y / z ]_ ( x e. B |-> X ) )
40 39 fveq1d 
 |-  ( z = y -> ( ( x e. B |-> X ) ` n ) = ( [_ y / z ]_ ( x e. B |-> X ) ` n ) )
41 35 38 40 cbvmpt 
 |-  ( z e. A |-> ( ( x e. B |-> X ) ` n ) ) = ( y e. A |-> ( [_ y / z ]_ ( x e. B |-> X ) ` n ) )
42 34 41 eqtrdi 
 |-  ( ( ph /\ n e. ( M ... N ) ) -> ( ( x e. B |-> ( z e. A |-> X ) ) ` n ) = ( y e. A |-> ( [_ y / z ]_ ( x e. B |-> X ) ` n ) ) )
43 1 2 42 seqof 
 |-  ( ph -> ( seq M ( oF .+ , ( x e. B |-> ( z e. A |-> X ) ) ) ` N ) = ( y e. A |-> ( seq M ( .+ , [_ y / z ]_ ( x e. B |-> X ) ) ` N ) ) )
44 nfcv 
 |-  F/_ y ( seq M ( .+ , ( x e. B |-> X ) ) ` N )
45 nfcv 
 |-  F/_ z M
46 nfcv 
 |-  F/_ z .+
47 45 46 36 nfseq 
 |-  F/_ z seq M ( .+ , [_ y / z ]_ ( x e. B |-> X ) )
48 nfcv 
 |-  F/_ z N
49 47 48 nffv 
 |-  F/_ z ( seq M ( .+ , [_ y / z ]_ ( x e. B |-> X ) ) ` N )
50 39 seqeq3d 
 |-  ( z = y -> seq M ( .+ , ( x e. B |-> X ) ) = seq M ( .+ , [_ y / z ]_ ( x e. B |-> X ) ) )
51 50 fveq1d 
 |-  ( z = y -> ( seq M ( .+ , ( x e. B |-> X ) ) ` N ) = ( seq M ( .+ , [_ y / z ]_ ( x e. B |-> X ) ) ` N ) )
52 44 49 51 cbvmpt 
 |-  ( z e. A |-> ( seq M ( .+ , ( x e. B |-> X ) ) ` N ) ) = ( y e. A |-> ( seq M ( .+ , [_ y / z ]_ ( x e. B |-> X ) ) ` N ) )
53 43 52 eqtr4di 
 |-  ( ph -> ( seq M ( oF .+ , ( x e. B |-> ( z e. A |-> X ) ) ) ` N ) = ( z e. A |-> ( seq M ( .+ , ( x e. B |-> X ) ) ` N ) ) )