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 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
seqof2.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
seqof2.3 ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ⊆ 𝐵 )
seqof2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) ) → 𝑋 ∈ 𝑊 )
Assertion seqof2 ( 𝜑 → ( seq 𝑀 ( ∘f + , ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ) ‘ 𝑁 ) = ( 𝑧 ∈ 𝐴 ↦ ( seq 𝑀 ( + , ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ) ‘ 𝑁 ) ) )

Proof

Step Hyp Ref Expression
1 seqof2.1 ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
2 seqof2.2 ⊢ ( 𝜑 → 𝑁 ∈ ( ℤ≥ ‘ 𝑀 ) )
3 seqof2.3 ⊢ ( 𝜑 → ( 𝑀 ... 𝑁 ) ⊆ 𝐵 )
4 seqof2.4 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑧 ∈ 𝐴 ) ) → 𝑋 ∈ 𝑊 )
5 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) )
6 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑛 )
7 nfcv ⊢ Ⅎ 𝑥 𝐴
8 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 )
9 7 8 nfmpt ⊢ Ⅎ 𝑥 ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) )
10 6 9 nfeq ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑛 ) = ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) )
11 5 10 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑛 ) = ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) ) )
12 eleq1w ⊢ ( 𝑥 = 𝑛 → ( 𝑥 ∈ ( 𝑀 ... 𝑁 ) ↔ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) )
13 12 anbi2d ⊢ ( 𝑥 = 𝑛 → ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) ↔ ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) ) )
14 fveq2 ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑛 ) )
15 fveq2 ⊢ ( 𝑥 = 𝑛 → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) )
16 15 mpteq2dv ⊢ ( 𝑥 = 𝑛 → ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) ) = ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) ) )
17 14 16 eqeq12d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑥 ) = ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) ) ↔ ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑛 ) = ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) ) ) )
18 13 17 imbi12d ⊢ ( 𝑥 = 𝑛 → ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑥 ) = ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) ) ) ↔ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑛 ) = ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) ) ) ) )
19 3 sselda ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝑥 ∈ 𝐵 )
20 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → 𝐴 ∈ 𝑉 )
21 20 mptexd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ∈ V )
22 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) = ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) )
23 22 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ∈ V ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑥 ) = ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) )
24 19 21 23 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑥 ) = ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) )
25 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑥 ∈ 𝐵 )
26 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝜑 )
27 simpr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑧 ∈ 𝐴 )
28 26 25 27 4 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑧 ∈ 𝐴 ) → 𝑋 ∈ 𝑊 )
29 eqid ⊢ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) = ( 𝑥 ∈ 𝐵 ↦ 𝑋 )
30 29 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐵 ∧ 𝑋 ∈ 𝑊 ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) = 𝑋 )
31 25 28 30 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) ∧ 𝑧 ∈ 𝐴 ) → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) = 𝑋 )
32 31 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) ) = ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) )
33 24 32 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑥 ) = ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑥 ) ) )
34 11 18 33 chvarfv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑛 ) = ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) ) )
35 nfcv ⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 )
36 nfcsb1v ⊢ Ⅎ 𝑧 ⦋ 𝑦 / 𝑧 ⦌ ( 𝑥 ∈ 𝐵 ↦ 𝑋 )
37 nfcv ⊢ Ⅎ 𝑧 𝑛
38 36 37 nffv ⊢ Ⅎ 𝑧 ( ⦋ 𝑦 / 𝑧 ⦌ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 )
39 csbeq1a ⊢ ( 𝑧 = 𝑦 → ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) = ⦋ 𝑦 / 𝑧 ⦌ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) )
40 39 fveq1d ⊢ ( 𝑧 = 𝑦 → ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) = ( ⦋ 𝑦 / 𝑧 ⦌ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) )
41 35 38 40 cbvmpt ⊢ ( 𝑧 ∈ 𝐴 ↦ ( ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) ) = ( 𝑦 ∈ 𝐴 ↦ ( ⦋ 𝑦 / 𝑧 ⦌ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) )
42 34 41 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 𝑀 ... 𝑁 ) ) → ( ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ‘ 𝑛 ) = ( 𝑦 ∈ 𝐴 ↦ ( ⦋ 𝑦 / 𝑧 ⦌ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ‘ 𝑛 ) ) )
43 1 2 42 seqof ⊢ ( 𝜑 → ( seq 𝑀 ( ∘f + , ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ) ‘ 𝑁 ) = ( 𝑦 ∈ 𝐴 ↦ ( seq 𝑀 ( + , ⦋ 𝑦 / 𝑧 ⦌ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ) ‘ 𝑁 ) ) )
44 nfcv ⊢ Ⅎ 𝑦 ( seq 𝑀 ( + , ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ) ‘ 𝑁 )
45 nfcv ⊢ Ⅎ 𝑧 𝑀
46 nfcv ⊢ Ⅎ 𝑧 +
47 45 46 36 nfseq ⊢ Ⅎ 𝑧 seq 𝑀 ( + , ⦋ 𝑦 / 𝑧 ⦌ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) )
48 nfcv ⊢ Ⅎ 𝑧 𝑁
49 47 48 nffv ⊢ Ⅎ 𝑧 ( seq 𝑀 ( + , ⦋ 𝑦 / 𝑧 ⦌ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ) ‘ 𝑁 )
50 39 seqeq3d ⊢ ( 𝑧 = 𝑦 → seq 𝑀 ( + , ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ) = seq 𝑀 ( + , ⦋ 𝑦 / 𝑧 ⦌ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ) )
51 50 fveq1d ⊢ ( 𝑧 = 𝑦 → ( seq 𝑀 ( + , ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ) ‘ 𝑁 ) = ( seq 𝑀 ( + , ⦋ 𝑦 / 𝑧 ⦌ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ) ‘ 𝑁 ) )
52 44 49 51 cbvmpt ⊢ ( 𝑧 ∈ 𝐴 ↦ ( seq 𝑀 ( + , ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ) ‘ 𝑁 ) ) = ( 𝑦 ∈ 𝐴 ↦ ( seq 𝑀 ( + , ⦋ 𝑦 / 𝑧 ⦌ ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ) ‘ 𝑁 ) )
53 43 52 eqtr4di ⊢ ( 𝜑 → ( seq 𝑀 ( ∘f + , ( 𝑥 ∈ 𝐵 ↦ ( 𝑧 ∈ 𝐴 ↦ 𝑋 ) ) ) ‘ 𝑁 ) = ( 𝑧 ∈ 𝐴 ↦ ( seq 𝑀 ( + , ( 𝑥 ∈ 𝐵 ↦ 𝑋 ) ) ‘ 𝑁 ) ) )