Metamath Proof Explorer

Theorem breprexplema

Description: Lemma for breprexp (induction step for weighted sums over representations). (Contributed by Thierry Arnoux, 7-Dec-2021)

Ref Expression
Hypotheses breprexp.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
breprexp.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
breprexplema.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
breprexplema.1 ⊢ ( 𝜑 → 𝑀 ≤ ( ( 𝑆 + 1 ) · 𝑁 ) )
breprexplema.l ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ )
Assertion breprexplema ( 𝜑 → Σ 𝑑 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑆 + 1 ) ) 𝑀 ) ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) = Σ 𝑏 ∈ ( 1 ... 𝑁 ) Σ 𝑑 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ) )

Proof

Step Hyp Ref Expression
1 breprexp.n ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
2 breprexp.s ⊢ ( 𝜑 → 𝑆 ∈ ℕ0 )
3 breprexplema.m ⊢ ( 𝜑 → 𝑀 ∈ ℕ0 )
4 breprexplema.1 ⊢ ( 𝜑 → 𝑀 ≤ ( ( 𝑆 + 1 ) · 𝑁 ) )
5 breprexplema.l ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) ∧ 𝑦 ∈ ℕ ) → ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ )
6 fz1ssnn ⊢ ( 1 ... 𝑁 ) ⊆ ℕ
7 6 a1i ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ⊆ ℕ )
8 3 nn0zd ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
9 eqid ⊢ ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) = ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
10 7 8 2 9 reprsuc ⊢ ( 𝜑 → ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑆 + 1 ) ) 𝑀 ) = ∪ 𝑏 ∈ ( 1 ... 𝑁 ) ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) )
11 10 sumeq1d ⊢ ( 𝜑 → Σ 𝑑 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑆 + 1 ) ) 𝑀 ) ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) = Σ 𝑑 ∈ ∪ 𝑏 ∈ ( 1 ... 𝑁 ) ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) )
12 fzfid ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ Fin )
13 6 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( 1 ... 𝑁 ) ⊆ ℕ )
14 8 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → 𝑀 ∈ ℤ )
15 fzssz ⊢ ( 1 ... 𝑁 ) ⊆ ℤ
16 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → 𝑏 ∈ ( 1 ... 𝑁 ) )
17 15 16 sselid ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → 𝑏 ∈ ℤ )
18 14 17 zsubcld ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( 𝑀 − 𝑏 ) ∈ ℤ )
19 2 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → 𝑆 ∈ ℕ0 )
20 12 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( 1 ... 𝑁 ) ∈ Fin )
21 13 18 19 20 reprfi ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ∈ Fin )
22 mptfi ⊢ ( ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ∈ Fin → ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∈ Fin )
23 21 22 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∈ Fin )
24 rnfi ⊢ ( ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∈ Fin → ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∈ Fin )
25 23 24 syl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∈ Fin )
26 13 18 19 reprval ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) = { 𝑐 ∈ ( ( 1 ... 𝑁 ) ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = ( 𝑀 − 𝑏 ) } )
27 ssrab2 ⊢ { 𝑐 ∈ ( ( 1 ... 𝑁 ) ↑m ( 0 ..^ 𝑆 ) ) ∣ Σ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( 𝑐 ‘ 𝑎 ) = ( 𝑀 − 𝑏 ) } ⊆ ( ( 1 ... 𝑁 ) ↑m ( 0 ..^ 𝑆 ) )
28 26 27 eqsstrdi ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ⊆ ( ( 1 ... 𝑁 ) ↑m ( 0 ..^ 𝑆 ) ) )
29 12 elexd ⊢ ( 𝜑 → ( 1 ... 𝑁 ) ∈ V )
30 fzonel ⊢ ¬ 𝑆 ∈ ( 0 ..^ 𝑆 )
31 30 a1i ⊢ ( 𝜑 → ¬ 𝑆 ∈ ( 0 ..^ 𝑆 ) )
32 28 29 2 31 9 actfunsnrndisj ⊢ ( 𝜑 → Disj 𝑏 ∈ ( 1 ... 𝑁 ) ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) )
33 fzofi ⊢ ( 0 ..^ ( 𝑆 + 1 ) ) ∈ Fin
34 33 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) → ( 0 ..^ ( 𝑆 + 1 ) ) ∈ Fin )
35 5 ralrimiva ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) → ∀ 𝑦 ∈ ℕ ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ )
36 35 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∀ 𝑦 ∈ ℕ ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ )
37 36 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) → ∀ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∀ 𝑦 ∈ ℕ ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ )
38 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) → 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) )
39 nfv ⊢ Ⅎ 𝑣 ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) )
40 nfcv ⊢ Ⅎ 𝑣 𝑑
41 nfmpt1 ⊢ Ⅎ 𝑣 ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
42 41 nfrn ⊢ Ⅎ 𝑣 ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
43 40 42 nfel ⊢ Ⅎ 𝑣 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
44 39 43 nfan ⊢ Ⅎ 𝑣 ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) )
45 6 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 1 ... 𝑁 ) ⊆ ℕ )
46 18 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑀 − 𝑏 ) ∈ ℤ )
47 19 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑆 ∈ ℕ0 )
48 simplr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) )
49 45 46 47 48 reprf ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑣 : ( 0 ..^ 𝑆 ) ⟶ ( 1 ... 𝑁 ) )
50 16 ad3antrrr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑏 ∈ ( 1 ... 𝑁 ) )
51 47 50 fsnd ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → { ⟨ 𝑆 , 𝑏 ⟩ } : { 𝑆 } ⟶ ( 1 ... 𝑁 ) )
52 fzodisjsn ⊢ ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅
53 52 a1i ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅ )
54 fun2 ⊢ ( ( ( 𝑣 : ( 0 ..^ 𝑆 ) ⟶ ( 1 ... 𝑁 ) ∧ { ⟨ 𝑆 , 𝑏 ⟩ } : { 𝑆 } ⟶ ( 1 ... 𝑁 ) ) ∧ ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅ ) → ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) : ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) ⟶ ( 1 ... 𝑁 ) )
55 49 51 53 54 syl21anc ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) : ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) ⟶ ( 1 ... 𝑁 ) )
56 simpr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
57 nn0uz ⊢ ℕ0 = ( ℤ≥ ‘ 0 )
58 2 57 eleqtrdi ⊢ ( 𝜑 → 𝑆 ∈ ( ℤ≥ ‘ 0 ) )
59 fzosplitsn ⊢ ( 𝑆 ∈ ( ℤ≥ ‘ 0 ) → ( 0 ..^ ( 𝑆 + 1 ) ) = ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) )
60 58 59 syl ⊢ ( 𝜑 → ( 0 ..^ ( 𝑆 + 1 ) ) = ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) )
61 60 ad4antr ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 0 ..^ ( 𝑆 + 1 ) ) = ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) )
62 56 61 feq12d ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → ( 𝑑 : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ ( 1 ... 𝑁 ) ↔ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) : ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) ⟶ ( 1 ... 𝑁 ) ) )
63 55 62 mpbird ⊢ ( ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) → 𝑑 : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ ( 1 ... 𝑁 ) )
64 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) → 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) )
65 vex ⊢ 𝑣 ∈ V
66 snex ⊢ { ⟨ 𝑆 , 𝑏 ⟩ } ∈ V
67 65 66 unex ⊢ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ∈ V
68 9 67 elrnmpti ⊢ ( 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ↔ ∃ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
69 64 68 sylib ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) → ∃ 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) 𝑑 = ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
70 44 63 69 r19.29af ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) → 𝑑 : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ ( 1 ... 𝑁 ) )
71 70 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) → 𝑑 : ( 0 ..^ ( 𝑆 + 1 ) ) ⟶ ( 1 ... 𝑁 ) )
72 71 38 ffvelcdmd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) → ( 𝑑 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) )
73 6 72 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) → ( 𝑑 ‘ 𝑎 ) ∈ ℕ )
74 fveq2 ⊢ ( 𝑥 = 𝑎 → ( 𝐿 ‘ 𝑥 ) = ( 𝐿 ‘ 𝑎 ) )
75 74 fveq1d ⊢ ( 𝑥 = 𝑎 → ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) = ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑦 ) )
76 75 eleq1d ⊢ ( 𝑥 = 𝑎 → ( ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ ↔ ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑦 ) ∈ ℂ ) )
77 fveq2 ⊢ ( 𝑦 = ( 𝑑 ‘ 𝑎 ) → ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑦 ) = ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) )
78 77 eleq1d ⊢ ( 𝑦 = ( 𝑑 ‘ 𝑎 ) → ( ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑦 ) ∈ ℂ ↔ ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) ∈ ℂ ) )
79 76 78 rspc2v ⊢ ( ( 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∧ ( 𝑑 ‘ 𝑎 ) ∈ ℕ ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∀ 𝑦 ∈ ℕ ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ → ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) ∈ ℂ ) )
80 38 73 79 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∀ 𝑦 ∈ ℕ ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ → ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) ∈ ℂ ) )
81 37 80 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ∧ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) → ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) ∈ ℂ )
82 34 81 fprodcl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) → ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) ∈ ℂ )
83 82 anasss ⊢ ( ( 𝜑 ∧ ( 𝑏 ∈ ( 1 ... 𝑁 ) ∧ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ) ) → ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) ∈ ℂ )
84 12 25 32 83 fsumiun ⊢ ( 𝜑 → Σ 𝑑 ∈ ∪ 𝑏 ∈ ( 1 ... 𝑁 ) ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) = Σ 𝑏 ∈ ( 1 ... 𝑁 ) Σ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) )
85 60 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( 0 ..^ ( 𝑆 + 1 ) ) = ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) )
86 85 prodeq1d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) = ∏ 𝑎 ∈ ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) )
87 nfv ⊢ Ⅎ 𝑎 ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) )
88 nfcv ⊢ Ⅎ 𝑎 ( ( 𝐿 ‘ 𝑆 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) )
89 fzofi ⊢ ( 0 ..^ 𝑆 ) ∈ Fin
90 89 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( 0 ..^ 𝑆 ) ∈ Fin )
91 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑆 ∈ ℕ0 )
92 30 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ¬ 𝑆 ∈ ( 0 ..^ 𝑆 ) )
93 6 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( 1 ... 𝑁 ) ⊆ ℕ )
94 18 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( 𝑀 − 𝑏 ) ∈ ℤ )
95 simpr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) )
96 93 94 91 95 reprf ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑒 : ( 0 ..^ 𝑆 ) ⟶ ( 1 ... 𝑁 ) )
97 96 ffnd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑒 Fn ( 0 ..^ 𝑆 ) )
98 97 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑒 Fn ( 0 ..^ 𝑆 ) )
99 16 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑏 ∈ ( 1 ... 𝑁 ) )
100 fnsng ⊢ ( ( 𝑆 ∈ ℕ0 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → { ⟨ 𝑆 , 𝑏 ⟩ } Fn { 𝑆 } )
101 91 99 100 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → { ⟨ 𝑆 , 𝑏 ⟩ } Fn { 𝑆 } )
102 101 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → { ⟨ 𝑆 , 𝑏 ⟩ } Fn { 𝑆 } )
103 52 a1i ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅ )
104 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( 0 ..^ 𝑆 ) )
105 fvun1 ⊢ ( ( 𝑒 Fn ( 0 ..^ 𝑆 ) ∧ { ⟨ 𝑆 , 𝑏 ⟩ } Fn { 𝑆 } ∧ ( ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅ ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) ) → ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) = ( 𝑒 ‘ 𝑎 ) )
106 98 102 103 104 105 syl112anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) = ( 𝑒 ‘ 𝑎 ) )
107 106 fveq2d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) = ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) )
108 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ∀ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∀ 𝑦 ∈ ℕ ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ )
109 108 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ∀ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∀ 𝑦 ∈ ℕ ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ )
110 fzossfzop1 ⊢ ( 𝑆 ∈ ℕ0 → ( 0 ..^ 𝑆 ) ⊆ ( 0 ..^ ( 𝑆 + 1 ) ) )
111 2 110 syl ⊢ ( 𝜑 → ( 0 ..^ 𝑆 ) ⊆ ( 0 ..^ ( 𝑆 + 1 ) ) )
112 111 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( 0 ..^ 𝑆 ) ⊆ ( 0 ..^ ( 𝑆 + 1 ) ) )
113 112 sselda ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) )
114 96 ffvelcdmda ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑒 ‘ 𝑎 ) ∈ ( 1 ... 𝑁 ) )
115 6 114 sselid ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑒 ‘ 𝑎 ) ∈ ℕ )
116 fveq2 ⊢ ( 𝑦 = ( 𝑒 ‘ 𝑎 ) → ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑦 ) = ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) )
117 116 eleq1d ⊢ ( 𝑦 = ( 𝑒 ‘ 𝑎 ) → ( ( ( 𝐿 ‘ 𝑎 ) ‘ 𝑦 ) ∈ ℂ ↔ ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) ∈ ℂ ) )
118 76 117 rspc2v ⊢ ( ( 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∧ ( 𝑒 ‘ 𝑎 ) ∈ ℕ ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∀ 𝑦 ∈ ℕ ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ → ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) ∈ ℂ ) )
119 113 115 118 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∀ 𝑦 ∈ ℕ ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ → ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) ∈ ℂ ) )
120 109 119 mpd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) ∈ ℂ )
121 107 120 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) ∈ ℂ )
122 fveq2 ⊢ ( 𝑎 = 𝑆 → ( 𝐿 ‘ 𝑎 ) = ( 𝐿 ‘ 𝑆 ) )
123 fveq2 ⊢ ( 𝑎 = 𝑆 → ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) = ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) )
124 122 123 fveq12d ⊢ ( 𝑎 = 𝑆 → ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) = ( ( 𝐿 ‘ 𝑆 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) ) )
125 52 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅ )
126 snidg ⊢ ( 𝑆 ∈ ℕ0 → 𝑆 ∈ { 𝑆 } )
127 91 126 syl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑆 ∈ { 𝑆 } )
128 fvun2 ⊢ ( ( 𝑒 Fn ( 0 ..^ 𝑆 ) ∧ { ⟨ 𝑆 , 𝑏 ⟩ } Fn { 𝑆 } ∧ ( ( ( 0 ..^ 𝑆 ) ∩ { 𝑆 } ) = ∅ ∧ 𝑆 ∈ { 𝑆 } ) ) → ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) = ( { ⟨ 𝑆 , 𝑏 ⟩ } ‘ 𝑆 ) )
129 97 101 125 127 128 syl112anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) = ( { ⟨ 𝑆 , 𝑏 ⟩ } ‘ 𝑆 ) )
130 fvsng ⊢ ( ( 𝑆 ∈ ℕ0 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( { ⟨ 𝑆 , 𝑏 ⟩ } ‘ 𝑆 ) = 𝑏 )
131 91 99 130 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( { ⟨ 𝑆 , 𝑏 ⟩ } ‘ 𝑆 ) = 𝑏 )
132 129 131 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) = 𝑏 )
133 132 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( ( 𝐿 ‘ 𝑆 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) ) = ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) )
134 fzonn0p1 ⊢ ( 𝑆 ∈ ℕ0 → 𝑆 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) )
135 2 134 syl ⊢ ( 𝜑 → 𝑆 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) )
136 135 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑆 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) )
137 6 99 sselid ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → 𝑏 ∈ ℕ )
138 fveq2 ⊢ ( 𝑥 = 𝑆 → ( 𝐿 ‘ 𝑥 ) = ( 𝐿 ‘ 𝑆 ) )
139 138 fveq1d ⊢ ( 𝑥 = 𝑆 → ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) = ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑦 ) )
140 139 eleq1d ⊢ ( 𝑥 = 𝑆 → ( ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ ↔ ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑦 ) ∈ ℂ ) )
141 fveq2 ⊢ ( 𝑦 = 𝑏 → ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑦 ) = ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) )
142 141 eleq1d ⊢ ( 𝑦 = 𝑏 → ( ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑦 ) ∈ ℂ ↔ ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ∈ ℂ ) )
143 140 142 rspc2v ⊢ ( ( 𝑆 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∧ 𝑏 ∈ ℕ ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∀ 𝑦 ∈ ℕ ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ → ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ∈ ℂ ) )
144 136 137 143 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( ∀ 𝑥 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ∀ 𝑦 ∈ ℕ ( ( 𝐿 ‘ 𝑥 ) ‘ 𝑦 ) ∈ ℂ → ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ∈ ℂ ) )
145 108 144 mpd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ∈ ℂ )
146 133 145 eqeltrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( ( 𝐿 ‘ 𝑆 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) ) ∈ ℂ )
147 87 88 90 91 92 121 124 146 fprodsplitsn ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ∏ 𝑎 ∈ ( ( 0 ..^ 𝑆 ) ∪ { 𝑆 } ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) ) ) )
148 107 prodeq2dv ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) )
149 148 133 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑆 ) ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ) )
150 86 147 149 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ) )
151 150 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) = Σ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ) )
152 simpl ⊢ ( ( 𝑑 = ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ∧ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) → 𝑑 = ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
153 152 fveq1d ⊢ ( ( 𝑑 = ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ∧ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) → ( 𝑑 ‘ 𝑎 ) = ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) )
154 153 fveq2d ⊢ ( ( 𝑑 = ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ∧ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ) → ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) = ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) )
155 154 prodeq2dv ⊢ ( 𝑑 = ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) → ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) = ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) )
156 28 29 2 31 9 actfunsnf1o ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) : ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) –1-1-onto→ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) )
157 9 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) = ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) )
158 simpr ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑣 = 𝑒 ) → 𝑣 = 𝑒 )
159 158 uneq1d ⊢ ( ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) ∧ 𝑣 = 𝑒 ) → ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) = ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
160 vex ⊢ 𝑒 ∈ V
161 160 66 unex ⊢ ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ∈ V
162 161 a1i ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ∈ V )
163 157 159 95 162 fvmptd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) ∧ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ) → ( ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ‘ 𝑒 ) = ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) )
164 155 21 156 163 82 fsumf1o ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) = Σ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( ( 𝑒 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ‘ 𝑎 ) ) )
165 simpl ⊢ ( ( 𝑑 = 𝑒 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → 𝑑 = 𝑒 )
166 165 fveq1d ⊢ ( ( 𝑑 = 𝑒 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( 𝑑 ‘ 𝑎 ) = ( 𝑒 ‘ 𝑎 ) )
167 166 fveq2d ⊢ ( ( 𝑑 = 𝑒 ∧ 𝑎 ∈ ( 0 ..^ 𝑆 ) ) → ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) = ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) )
168 167 prodeq2dv ⊢ ( 𝑑 = 𝑒 → ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) = ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) )
169 168 oveq1d ⊢ ( 𝑑 = 𝑒 → ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ) = ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ) )
170 169 cbvsumv ⊢ Σ 𝑑 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ) = Σ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) )
171 170 a1i ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑑 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ) = Σ 𝑒 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑒 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ) )
172 151 164 171 3eqtr4d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ ( 1 ... 𝑁 ) ) → Σ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) = Σ 𝑑 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ) )
173 172 sumeq2dv ⊢ ( 𝜑 → Σ 𝑏 ∈ ( 1 ... 𝑁 ) Σ 𝑑 ∈ ran ( 𝑣 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ↦ ( 𝑣 ∪ { ⟨ 𝑆 , 𝑏 ⟩ } ) ) ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) = Σ 𝑏 ∈ ( 1 ... 𝑁 ) Σ 𝑑 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ) )
174 11 84 173 3eqtrd ⊢ ( 𝜑 → Σ 𝑑 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ ( 𝑆 + 1 ) ) 𝑀 ) ∏ 𝑎 ∈ ( 0 ..^ ( 𝑆 + 1 ) ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) = Σ 𝑏 ∈ ( 1 ... 𝑁 ) Σ 𝑑 ∈ ( ( 1 ... 𝑁 ) ( repr ‘ 𝑆 ) ( 𝑀 − 𝑏 ) ) ( ∏ 𝑎 ∈ ( 0 ..^ 𝑆 ) ( ( 𝐿 ‘ 𝑎 ) ‘ ( 𝑑 ‘ 𝑎 ) ) · ( ( 𝐿 ‘ 𝑆 ) ‘ 𝑏 ) ) )