Mathbox for Thierry Arnoux < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  breprexplema Structured version   Visualization version   GIF version

Theorem breprexplema 30836
 Description: Lemma for breprexp 30839 (induction step for weighted sums over representations) (Contributed by Thierry Arnoux, 7-Dec-2021.)
Hypotheses
Ref Expression
breprexp.n (𝜑𝑁 ∈ ℕ0)
breprexp.s (𝜑𝑆 ∈ ℕ0)
breprexplema.m (𝜑𝑀 ∈ ℕ0)
breprexplema.1 (𝜑𝑀 ≤ ((𝑆 + 1) · 𝑁))
breprexplema.l (((𝜑𝑥 ∈ (0..^(𝑆 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿𝑥)‘𝑦) ∈ ℂ)
Assertion
Ref Expression
breprexplema (𝜑 → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑆 + 1))𝑀)∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑆)‘𝑏)))
Distinct variable groups:   𝑆,𝑎   𝐿,𝑎,𝑏,𝑑,𝑥,𝑦   𝑀,𝑎,𝑏,𝑑   𝑁,𝑎,𝑏,𝑑   𝑆,𝑏,𝑑,𝑥,𝑦   𝜑,𝑎,𝑏,𝑑,𝑥,𝑦
Allowed substitution hints:   𝑀(𝑥,𝑦)   𝑁(𝑥,𝑦)

Proof of Theorem breprexplema
Dummy variables 𝑐 𝑒 𝑣 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fz1ssnn 12410 . . . . 5 (1...𝑁) ⊆ ℕ
21a1i 11 . . . 4 (𝜑 → (1...𝑁) ⊆ ℕ)
3 breprexplema.m . . . . 5 (𝜑𝑀 ∈ ℕ0)
43nn0zd 11518 . . . 4 (𝜑𝑀 ∈ ℤ)
5 breprexp.s . . . 4 (𝜑𝑆 ∈ ℕ0)
6 eqid 2651 . . . 4 (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) = (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
72, 4, 5, 6reprsuc 30821 . . 3 (𝜑 → ((1...𝑁)(repr‘(𝑆 + 1))𝑀) = 𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))
87sumeq1d 14475 . 2 (𝜑 → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑆 + 1))𝑀)∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)))
9 fzfid 12812 . . 3 (𝜑 → (1...𝑁) ∈ Fin)
101a1i 11 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → (1...𝑁) ⊆ ℕ)
114adantr 480 . . . . . . 7 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑀 ∈ ℤ)
12 fzssz 12381 . . . . . . . 8 (1...𝑁) ⊆ ℤ
13 simpr 476 . . . . . . . 8 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑏 ∈ (1...𝑁))
1412, 13sseldi 3634 . . . . . . 7 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑏 ∈ ℤ)
1511, 14zsubcld 11525 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → (𝑀𝑏) ∈ ℤ)
165adantr 480 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → 𝑆 ∈ ℕ0)
179adantr 480 . . . . . 6 ((𝜑𝑏 ∈ (1...𝑁)) → (1...𝑁) ∈ Fin)
1810, 15, 16, 17reprfi 30822 . . . . 5 ((𝜑𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ∈ Fin)
19 mptfi 8306 . . . . 5 (((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ∈ Fin → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) ∈ Fin)
2018, 19syl 17 . . . 4 ((𝜑𝑏 ∈ (1...𝑁)) → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) ∈ Fin)
21 rnfi 8290 . . . 4 ((𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) ∈ Fin → ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) ∈ Fin)
2220, 21syl 17 . . 3 ((𝜑𝑏 ∈ (1...𝑁)) → ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) ∈ Fin)
2310, 15, 16reprval 30816 . . . . 5 ((𝜑𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) = {𝑐 ∈ ((1...𝑁) ↑𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = (𝑀𝑏)})
24 ssrab2 3720 . . . . 5 {𝑐 ∈ ((1...𝑁) ↑𝑚 (0..^𝑆)) ∣ Σ𝑎 ∈ (0..^𝑆)(𝑐𝑎) = (𝑀𝑏)} ⊆ ((1...𝑁) ↑𝑚 (0..^𝑆))
2523, 24syl6eqss 3688 . . . 4 ((𝜑𝑏 ∈ (1...𝑁)) → ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ⊆ ((1...𝑁) ↑𝑚 (0..^𝑆)))
269elexd 3245 . . . 4 (𝜑 → (1...𝑁) ∈ V)
27 fzonel 12522 . . . . 5 ¬ 𝑆 ∈ (0..^𝑆)
2827a1i 11 . . . 4 (𝜑 → ¬ 𝑆 ∈ (0..^𝑆))
2925, 26, 5, 28, 6actfunsnrndisj 30811 . . 3 (𝜑Disj 𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))
30 fzofi 12813 . . . . . 6 (0..^(𝑆 + 1)) ∈ Fin
3130a1i 11 . . . . 5 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) → (0..^(𝑆 + 1)) ∈ Fin)
32 breprexplema.l . . . . . . . . 9 (((𝜑𝑥 ∈ (0..^(𝑆 + 1))) ∧ 𝑦 ∈ ℕ) → ((𝐿𝑥)‘𝑦) ∈ ℂ)
3332ralrimiva 2995 . . . . . . . 8 ((𝜑𝑥 ∈ (0..^(𝑆 + 1))) → ∀𝑦 ∈ ℕ ((𝐿𝑥)‘𝑦) ∈ ℂ)
3433ralrimiva 2995 . . . . . . 7 (𝜑 → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿𝑥)‘𝑦) ∈ ℂ)
3534ad3antrrr 766 . . . . . 6 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿𝑥)‘𝑦) ∈ ℂ)
36 simpr 476 . . . . . . 7 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → 𝑎 ∈ (0..^(𝑆 + 1)))
37 nfv 1883 . . . . . . . . . . . 12 𝑣(𝜑𝑏 ∈ (1...𝑁))
38 nfcv 2793 . . . . . . . . . . . . 13 𝑣𝑑
39 nfmpt1 4780 . . . . . . . . . . . . . 14 𝑣(𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
4039nfrn 5400 . . . . . . . . . . . . 13 𝑣ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
4138, 40nfel 2806 . . . . . . . . . . . 12 𝑣 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
4237, 41nfan 1868 . . . . . . . . . . 11 𝑣((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))
431a1i 11 . . . . . . . . . . . . . 14 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → (1...𝑁) ⊆ ℕ)
4415ad3antrrr 766 . . . . . . . . . . . . . 14 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → (𝑀𝑏) ∈ ℤ)
4516ad3antrrr 766 . . . . . . . . . . . . . 14 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → 𝑆 ∈ ℕ0)
46 simplr 807 . . . . . . . . . . . . . 14 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)))
4743, 44, 45, 46reprf 30818 . . . . . . . . . . . . 13 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → 𝑣:(0..^𝑆)⟶(1...𝑁))
4813ad3antrrr 766 . . . . . . . . . . . . . 14 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → 𝑏 ∈ (1...𝑁))
4945, 48fsnd 6217 . . . . . . . . . . . . 13 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → {⟨𝑆, 𝑏⟩}:{𝑆}⟶(1...𝑁))
50 fzodisjsn 12545 . . . . . . . . . . . . . 14 ((0..^𝑆) ∩ {𝑆}) = ∅
5150a1i 11 . . . . . . . . . . . . 13 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → ((0..^𝑆) ∩ {𝑆}) = ∅)
52 fun2 6105 . . . . . . . . . . . . 13 (((𝑣:(0..^𝑆)⟶(1...𝑁) ∧ {⟨𝑆, 𝑏⟩}:{𝑆}⟶(1...𝑁)) ∧ ((0..^𝑆) ∩ {𝑆}) = ∅) → (𝑣 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶(1...𝑁))
5347, 49, 51, 52syl21anc 1365 . . . . . . . . . . . 12 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → (𝑣 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶(1...𝑁))
54 simpr 476 . . . . . . . . . . . . 13 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
55 nn0uz 11760 . . . . . . . . . . . . . . . 16 0 = (ℤ‘0)
565, 55syl6eleq 2740 . . . . . . . . . . . . . . 15 (𝜑𝑆 ∈ (ℤ‘0))
57 fzosplitsn 12616 . . . . . . . . . . . . . . 15 (𝑆 ∈ (ℤ‘0) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
5856, 57syl 17 . . . . . . . . . . . . . 14 (𝜑 → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
5958ad4antr 769 . . . . . . . . . . . . 13 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
6054, 59feq12d 6071 . . . . . . . . . . . 12 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → (𝑑:(0..^(𝑆 + 1))⟶(1...𝑁) ↔ (𝑣 ∪ {⟨𝑆, 𝑏⟩}):((0..^𝑆) ∪ {𝑆})⟶(1...𝑁)))
6153, 60mpbird 247 . . . . . . . . . . 11 (((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩})) → 𝑑:(0..^(𝑆 + 1))⟶(1...𝑁))
62 simpr 476 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) → 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))
63 vex 3234 . . . . . . . . . . . . . 14 𝑣 ∈ V
64 snex 4938 . . . . . . . . . . . . . 14 {⟨𝑆, 𝑏⟩} ∈ V
6563, 64unex 6998 . . . . . . . . . . . . 13 (𝑣 ∪ {⟨𝑆, 𝑏⟩}) ∈ V
666, 65elrnmpti 5408 . . . . . . . . . . . 12 (𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) ↔ ∃𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
6762, 66sylib 208 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) → ∃𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))𝑑 = (𝑣 ∪ {⟨𝑆, 𝑏⟩}))
6842, 61, 67r19.29af 3105 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) → 𝑑:(0..^(𝑆 + 1))⟶(1...𝑁))
6968adantr 480 . . . . . . . . 9 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → 𝑑:(0..^(𝑆 + 1))⟶(1...𝑁))
7069, 36ffvelrnd 6400 . . . . . . . 8 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (𝑑𝑎) ∈ (1...𝑁))
711, 70sseldi 3634 . . . . . . 7 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (𝑑𝑎) ∈ ℕ)
72 fveq2 6229 . . . . . . . . . 10 (𝑥 = 𝑎 → (𝐿𝑥) = (𝐿𝑎))
7372fveq1d 6231 . . . . . . . . 9 (𝑥 = 𝑎 → ((𝐿𝑥)‘𝑦) = ((𝐿𝑎)‘𝑦))
7473eleq1d 2715 . . . . . . . 8 (𝑥 = 𝑎 → (((𝐿𝑥)‘𝑦) ∈ ℂ ↔ ((𝐿𝑎)‘𝑦) ∈ ℂ))
75 fveq2 6229 . . . . . . . . 9 (𝑦 = (𝑑𝑎) → ((𝐿𝑎)‘𝑦) = ((𝐿𝑎)‘(𝑑𝑎)))
7675eleq1d 2715 . . . . . . . 8 (𝑦 = (𝑑𝑎) → (((𝐿𝑎)‘𝑦) ∈ ℂ ↔ ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ))
7774, 76rspc2v 3353 . . . . . . 7 ((𝑎 ∈ (0..^(𝑆 + 1)) ∧ (𝑑𝑎) ∈ ℕ) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿𝑥)‘𝑦) ∈ ℂ → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ))
7836, 71, 77syl2anc 694 . . . . . 6 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿𝑥)‘𝑦) ∈ ℂ → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ))
7935, 78mpd 15 . . . . 5 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → ((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
8031, 79fprodcl 14726 . . . 4 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
8180anasss 680 . . 3 ((𝜑 ∧ (𝑏 ∈ (1...𝑁) ∧ 𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)) ∈ ℂ)
829, 22, 29, 81fsumiun 14597 . 2 (𝜑 → Σ𝑑 𝑏 ∈ (1...𝑁)ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)))
8358ad2antrr 762 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → (0..^(𝑆 + 1)) = ((0..^𝑆) ∪ {𝑆}))
8483prodeq1d 14695 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = ∏𝑎 ∈ ((0..^𝑆) ∪ {𝑆})((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)))
85 nfv 1883 . . . . . . 7 𝑎((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)))
86 nfcv 2793 . . . . . . 7 𝑎((𝐿𝑆)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))
87 fzofi 12813 . . . . . . . 8 (0..^𝑆) ∈ Fin
8887a1i 11 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → (0..^𝑆) ∈ Fin)
8916adantr 480 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → 𝑆 ∈ ℕ0)
9027a1i 11 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ¬ 𝑆 ∈ (0..^𝑆))
911a1i 11 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → (1...𝑁) ⊆ ℕ)
9215adantr 480 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → (𝑀𝑏) ∈ ℤ)
93 simpr 476 . . . . . . . . . . . . 13 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)))
9491, 92, 89, 93reprf 30818 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → 𝑒:(0..^𝑆)⟶(1...𝑁))
95 ffn 6083 . . . . . . . . . . . 12 (𝑒:(0..^𝑆)⟶(1...𝑁) → 𝑒 Fn (0..^𝑆))
9694, 95syl 17 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → 𝑒 Fn (0..^𝑆))
9796adantr 480 . . . . . . . . . 10 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑒 Fn (0..^𝑆))
9813adantr 480 . . . . . . . . . . . 12 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → 𝑏 ∈ (1...𝑁))
99 fnsng 5976 . . . . . . . . . . . 12 ((𝑆 ∈ ℕ0𝑏 ∈ (1...𝑁)) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
10089, 98, 99syl2anc 694 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
101100adantr 480 . . . . . . . . . 10 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → {⟨𝑆, 𝑏⟩} Fn {𝑆})
10250a1i 11 . . . . . . . . . 10 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((0..^𝑆) ∩ {𝑆}) = ∅)
103 simpr 476 . . . . . . . . . 10 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^𝑆))
104 fvun1 6308 . . . . . . . . . 10 ((𝑒 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑎 ∈ (0..^𝑆))) → ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑒𝑎))
10597, 101, 102, 103, 104syl112anc 1370 . . . . . . . . 9 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = (𝑒𝑎))
106105fveq2d 6233 . . . . . . . 8 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = ((𝐿𝑎)‘(𝑒𝑎)))
10734ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿𝑥)‘𝑦) ∈ ℂ)
108107adantr 480 . . . . . . . . 9 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿𝑥)‘𝑦) ∈ ℂ)
109 fzossfzop1 12585 . . . . . . . . . . . . 13 (𝑆 ∈ ℕ0 → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
1105, 109syl 17 . . . . . . . . . . . 12 (𝜑 → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
111110ad2antrr 762 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → (0..^𝑆) ⊆ (0..^(𝑆 + 1)))
112111sselda 3636 . . . . . . . . . 10 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → 𝑎 ∈ (0..^(𝑆 + 1)))
11394ffvelrnda 6399 . . . . . . . . . . 11 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ (1...𝑁))
1141, 113sseldi 3634 . . . . . . . . . 10 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → (𝑒𝑎) ∈ ℕ)
115 fveq2 6229 . . . . . . . . . . . 12 (𝑦 = (𝑒𝑎) → ((𝐿𝑎)‘𝑦) = ((𝐿𝑎)‘(𝑒𝑎)))
116115eleq1d 2715 . . . . . . . . . . 11 (𝑦 = (𝑒𝑎) → (((𝐿𝑎)‘𝑦) ∈ ℂ ↔ ((𝐿𝑎)‘(𝑒𝑎)) ∈ ℂ))
11774, 116rspc2v 3353 . . . . . . . . . 10 ((𝑎 ∈ (0..^(𝑆 + 1)) ∧ (𝑒𝑎) ∈ ℕ) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿𝑥)‘𝑦) ∈ ℂ → ((𝐿𝑎)‘(𝑒𝑎)) ∈ ℂ))
118112, 114, 117syl2anc 694 . . . . . . . . 9 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿𝑥)‘𝑦) ∈ ℂ → ((𝐿𝑎)‘(𝑒𝑎)) ∈ ℂ))
119108, 118mpd 15 . . . . . . . 8 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿𝑎)‘(𝑒𝑎)) ∈ ℂ)
120106, 119eqeltrd 2730 . . . . . . 7 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑎 ∈ (0..^𝑆)) → ((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) ∈ ℂ)
121 fveq2 6229 . . . . . . . 8 (𝑎 = 𝑆 → (𝐿𝑎) = (𝐿𝑆))
122 fveq2 6229 . . . . . . . 8 (𝑎 = 𝑆 → ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎) = ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))
123121, 122fveq12d 6235 . . . . . . 7 (𝑎 = 𝑆 → ((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = ((𝐿𝑆)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆)))
12450a1i 11 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ((0..^𝑆) ∩ {𝑆}) = ∅)
125 snidg 4239 . . . . . . . . . . . 12 (𝑆 ∈ ℕ0𝑆 ∈ {𝑆})
12689, 125syl 17 . . . . . . . . . . 11 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → 𝑆 ∈ {𝑆})
127 fvun2 6309 . . . . . . . . . . 11 ((𝑒 Fn (0..^𝑆) ∧ {⟨𝑆, 𝑏⟩} Fn {𝑆} ∧ (((0..^𝑆) ∩ {𝑆}) = ∅ ∧ 𝑆 ∈ {𝑆})) → ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
12896, 100, 124, 126, 127syl112anc 1370 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = ({⟨𝑆, 𝑏⟩}‘𝑆))
129 fvsng 6488 . . . . . . . . . . 11 ((𝑆 ∈ ℕ0𝑏 ∈ (1...𝑁)) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
13089, 98, 129syl2anc 694 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ({⟨𝑆, 𝑏⟩}‘𝑆) = 𝑏)
131128, 130eqtrd 2685 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆) = 𝑏)
132131fveq2d 6233 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ((𝐿𝑆)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆)) = ((𝐿𝑆)‘𝑏))
133 fzonn0p1 12584 . . . . . . . . . . . 12 (𝑆 ∈ ℕ0𝑆 ∈ (0..^(𝑆 + 1)))
1345, 133syl 17 . . . . . . . . . . 11 (𝜑𝑆 ∈ (0..^(𝑆 + 1)))
135134ad2antrr 762 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → 𝑆 ∈ (0..^(𝑆 + 1)))
1361, 98sseldi 3634 . . . . . . . . . 10 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → 𝑏 ∈ ℕ)
137 fveq2 6229 . . . . . . . . . . . . 13 (𝑥 = 𝑆 → (𝐿𝑥) = (𝐿𝑆))
138137fveq1d 6231 . . . . . . . . . . . 12 (𝑥 = 𝑆 → ((𝐿𝑥)‘𝑦) = ((𝐿𝑆)‘𝑦))
139138eleq1d 2715 . . . . . . . . . . 11 (𝑥 = 𝑆 → (((𝐿𝑥)‘𝑦) ∈ ℂ ↔ ((𝐿𝑆)‘𝑦) ∈ ℂ))
140 fveq2 6229 . . . . . . . . . . . 12 (𝑦 = 𝑏 → ((𝐿𝑆)‘𝑦) = ((𝐿𝑆)‘𝑏))
141140eleq1d 2715 . . . . . . . . . . 11 (𝑦 = 𝑏 → (((𝐿𝑆)‘𝑦) ∈ ℂ ↔ ((𝐿𝑆)‘𝑏) ∈ ℂ))
142139, 141rspc2v 3353 . . . . . . . . . 10 ((𝑆 ∈ (0..^(𝑆 + 1)) ∧ 𝑏 ∈ ℕ) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿𝑥)‘𝑦) ∈ ℂ → ((𝐿𝑆)‘𝑏) ∈ ℂ))
143135, 136, 142syl2anc 694 . . . . . . . . 9 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → (∀𝑥 ∈ (0..^(𝑆 + 1))∀𝑦 ∈ ℕ ((𝐿𝑥)‘𝑦) ∈ ℂ → ((𝐿𝑆)‘𝑏) ∈ ℂ))
144107, 143mpd 15 . . . . . . . 8 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ((𝐿𝑆)‘𝑏) ∈ ℂ)
145132, 144eqeltrd 2730 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ((𝐿𝑆)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆)) ∈ ℂ)
14685, 86, 88, 89, 90, 120, 123, 145fprodsplitsn 14764 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ∏𝑎 ∈ ((0..^𝑆) ∪ {𝑆})((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = (∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) · ((𝐿𝑆)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))))
147106prodeq2dv 14697 . . . . . . 7 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = ∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑒𝑎)))
148147, 132oveq12d 6708 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → (∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) · ((𝐿𝑆)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑆))) = (∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑒𝑎)) · ((𝐿𝑆)‘𝑏)))
14984, 146, 1483eqtrd 2689 . . . . 5 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = (∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑒𝑎)) · ((𝐿𝑆)‘𝑏)))
150149sumeq2dv 14477 . . . 4 ((𝜑𝑏 ∈ (1...𝑁)) → Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑒𝑎)) · ((𝐿𝑆)‘𝑏)))
151 simpl 472 . . . . . . . 8 ((𝑑 = (𝑒 ∪ {⟨𝑆, 𝑏⟩}) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → 𝑑 = (𝑒 ∪ {⟨𝑆, 𝑏⟩}))
152151fveq1d 6231 . . . . . . 7 ((𝑑 = (𝑒 ∪ {⟨𝑆, 𝑏⟩}) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → (𝑑𝑎) = ((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎))
153152fveq2d 6233 . . . . . 6 ((𝑑 = (𝑒 ∪ {⟨𝑆, 𝑏⟩}) ∧ 𝑎 ∈ (0..^(𝑆 + 1))) → ((𝐿𝑎)‘(𝑑𝑎)) = ((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)))
154153prodeq2dv 14697 . . . . 5 (𝑑 = (𝑒 ∪ {⟨𝑆, 𝑏⟩}) → ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)) = ∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)))
15525, 26, 5, 28, 6actfunsnf1o 30810 . . . . 5 ((𝜑𝑏 ∈ (1...𝑁)) → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})):((1...𝑁)(repr‘𝑆)(𝑀𝑏))–1-1-onto→ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))
1566a1i 11 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})) = (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩})))
157 simpr 476 . . . . . . 7 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑣 = 𝑒) → 𝑣 = 𝑒)
158157uneq1d 3799 . . . . . 6 ((((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) ∧ 𝑣 = 𝑒) → (𝑣 ∪ {⟨𝑆, 𝑏⟩}) = (𝑒 ∪ {⟨𝑆, 𝑏⟩}))
159 vex 3234 . . . . . . . 8 𝑒 ∈ V
160159, 64unex 6998 . . . . . . 7 (𝑒 ∪ {⟨𝑆, 𝑏⟩}) ∈ V
161160a1i 11 . . . . . 6 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → (𝑒 ∪ {⟨𝑆, 𝑏⟩}) ∈ V)
162156, 158, 93, 161fvmptd 6327 . . . . 5 (((𝜑𝑏 ∈ (1...𝑁)) ∧ 𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))) → ((𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))‘𝑒) = (𝑒 ∪ {⟨𝑆, 𝑏⟩}))
163154, 18, 155, 162, 80fsumf1o 14498 . . . 4 ((𝜑𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘((𝑒 ∪ {⟨𝑆, 𝑏⟩})‘𝑎)))
164 simpl 472 . . . . . . . . . 10 ((𝑑 = 𝑒𝑎 ∈ (0..^𝑆)) → 𝑑 = 𝑒)
165164fveq1d 6231 . . . . . . . . 9 ((𝑑 = 𝑒𝑎 ∈ (0..^𝑆)) → (𝑑𝑎) = (𝑒𝑎))
166165fveq2d 6233 . . . . . . . 8 ((𝑑 = 𝑒𝑎 ∈ (0..^𝑆)) → ((𝐿𝑎)‘(𝑑𝑎)) = ((𝐿𝑎)‘(𝑒𝑎)))
167166prodeq2dv 14697 . . . . . . 7 (𝑑 = 𝑒 → ∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑑𝑎)) = ∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑒𝑎)))
168167oveq1d 6705 . . . . . 6 (𝑑 = 𝑒 → (∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑆)‘𝑏)) = (∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑒𝑎)) · ((𝐿𝑆)‘𝑏)))
169168cbvsumv 14470 . . . . 5 Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑆)‘𝑏)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑒𝑎)) · ((𝐿𝑆)‘𝑏))
170169a1i 11 . . . 4 ((𝜑𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑆)‘𝑏)) = Σ𝑒 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑒𝑎)) · ((𝐿𝑆)‘𝑏)))
171150, 163, 1703eqtr4d 2695 . . 3 ((𝜑𝑏 ∈ (1...𝑁)) → Σ𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑆)‘𝑏)))
172171sumeq2dv 14477 . 2 (𝜑 → Σ𝑏 ∈ (1...𝑁𝑑 ∈ ran (𝑣 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏)) ↦ (𝑣 ∪ {⟨𝑆, 𝑏⟩}))∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑆)‘𝑏)))
1738, 82, 1723eqtrd 2689 1 (𝜑 → Σ𝑑 ∈ ((1...𝑁)(repr‘(𝑆 + 1))𝑀)∏𝑎 ∈ (0..^(𝑆 + 1))((𝐿𝑎)‘(𝑑𝑎)) = Σ𝑏 ∈ (1...𝑁𝑑 ∈ ((1...𝑁)(repr‘𝑆)(𝑀𝑏))(∏𝑎 ∈ (0..^𝑆)((𝐿𝑎)‘(𝑑𝑎)) · ((𝐿𝑆)‘𝑏)))
 Colors of variables: wff setvar class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 383   = wceq 1523   ∈ wcel 2030  ∀wral 2941  ∃wrex 2942  {crab 2945  Vcvv 3231   ∪ cun 3605   ∩ cin 3606   ⊆ wss 3607  ∅c0 3948  {csn 4210  ⟨cop 4216  ∪ ciun 4552   class class class wbr 4685   ↦ cmpt 4762  ran crn 5144   Fn wfn 5921  ⟶wf 5922  ‘cfv 5926  (class class class)co 6690   ↑𝑚 cmap 7899  Fincfn 7997  ℂcc 9972  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979   ≤ cle 10113   − cmin 10304  ℕcn 11058  ℕ0cn0 11330  ℤcz 11415  ℤ≥cuz 11725  ...cfz 12364  ..^cfzo 12504  Σcsu 14460  ∏cprod 14679  reprcrepr 30814 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-inf2 8576  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-fal 1529  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-disj 4653  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-se 5103  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-isom 5935  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-1o 7605  df-2o 7606  df-oadd 7609  df-er 7787  df-map 7901  df-pm 7902  df-en 7998  df-dom 7999  df-sdom 8000  df-fin 8001  df-sup 8389  df-oi 8456  df-card 8803  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-3 11118  df-n0 11331  df-z 11416  df-uz 11726  df-rp 11871  df-fz 12365  df-fzo 12505  df-seq 12842  df-exp 12901  df-hash 13158  df-cj 13883  df-re 13884  df-im 13885  df-sqrt 14019  df-abs 14020  df-clim 14263  df-sum 14461  df-prod 14680  df-repr 30815 This theorem is referenced by:  breprexplemc  30838
 Copyright terms: Public domain W3C validator