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 φ A V
seqof2.2 φ N M
seqof2.3 φ M N B
seqof2.4 φ x B z A X W
Assertion seqof2 φ seq M f + ˙ x B z A X N = z A seq M + ˙ x B X N

Proof

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