This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvmptfprodlem

Description: Induction step for dvmptfprod . (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvmptfprodlem.xph ⊢ Ⅎ 𝑥 𝜑
dvmptfprodlem.iph ⊢ Ⅎ 𝑖 𝜑
dvmptfprodlem.jph ⊢ Ⅎ 𝑗 𝜑
dvmptfprodlem.if ⊢ Ⅎ 𝑖 𝐹
dvmptfprodlem.jg ⊢ Ⅎ 𝑗 𝐺
dvmptfprodlem.a ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvmptfprodlem.d ⊢ ( 𝜑 → 𝐷 ∈ Fin )
dvmptfprodlem.e ⊢ ( 𝜑 → 𝐸 ∈ V )
dvmptfprodlem.db ⊢ ( 𝜑 → ¬ 𝐸 ∈ 𝐷 )
dvmptfprodlem.ss ⊢ ( 𝜑 → ( 𝐷 ∪ { 𝐸 } ) ⊆ 𝐼 )
dvmptfprodlem.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptfprodlem.c ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → 𝐶 ∈ ℂ )
dvmptfprodlem.dvp ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝐷 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) ) )
dvmptfprodlem.14 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐺 ∈ ℂ )
dvmptfprodlem.dvf ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐹 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐺 ) )
dvmptfprodlem.f ⊢ ( 𝑖 = 𝐸 → 𝐴 = 𝐹 )
dvmptfprodlem.cg ⊢ ( 𝑗 = 𝐸 → 𝐶 = 𝐺 )
Assertion dvmptfprodlem ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ ( 𝐷 ∪ { 𝐸 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) ) )

Proof

Step Hyp Ref Expression
1 dvmptfprodlem.xph ⊢ Ⅎ 𝑥 𝜑
2 dvmptfprodlem.iph ⊢ Ⅎ 𝑖 𝜑
3 dvmptfprodlem.jph ⊢ Ⅎ 𝑗 𝜑
4 dvmptfprodlem.if ⊢ Ⅎ 𝑖 𝐹
5 dvmptfprodlem.jg ⊢ Ⅎ 𝑗 𝐺
6 dvmptfprodlem.a ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
7 dvmptfprodlem.d ⊢ ( 𝜑 → 𝐷 ∈ Fin )
8 dvmptfprodlem.e ⊢ ( 𝜑 → 𝐸 ∈ V )
9 dvmptfprodlem.db ⊢ ( 𝜑 → ¬ 𝐸 ∈ 𝐷 )
10 dvmptfprodlem.ss ⊢ ( 𝜑 → ( 𝐷 ∪ { 𝐸 } ) ⊆ 𝐼 )
11 dvmptfprodlem.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
12 dvmptfprodlem.c ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → 𝐶 ∈ ℂ )
13 dvmptfprodlem.dvp ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ 𝐷 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) ) )
14 dvmptfprodlem.14 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐺 ∈ ℂ )
15 dvmptfprodlem.dvf ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐹 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐺 ) )
16 dvmptfprodlem.f ⊢ ( 𝑖 = 𝐸 → 𝐴 = 𝐹 )
17 dvmptfprodlem.cg ⊢ ( 𝑗 = 𝐸 → 𝐶 = 𝐺 )
18 nfcv ⊢ Ⅎ 𝑖 𝑥
19 nfcv ⊢ Ⅎ 𝑖 𝑋
20 18 19 nfel ⊢ Ⅎ 𝑖 𝑥 ∈ 𝑋
21 2 20 nfan ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝑥 ∈ 𝑋 )
22 4 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Ⅎ 𝑖 𝐹 )
23 snfi ⊢ { 𝐸 } ∈ Fin
24 23 a1i ⊢ ( 𝜑 → { 𝐸 } ∈ Fin )
25 unfi ⊢ ( ( 𝐷 ∈ Fin ∧ { 𝐸 } ∈ Fin ) → ( 𝐷 ∪ { 𝐸 } ) ∈ Fin )
26 7 24 25 syl2anc ⊢ ( 𝜑 → ( 𝐷 ∪ { 𝐸 } ) ∈ Fin )
27 26 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐷 ∪ { 𝐸 } ) ∈ Fin )
28 simpll ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) ) → 𝜑 )
29 10 sselda ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) ) → 𝑖 ∈ 𝐼 )
30 29 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) ) → 𝑖 ∈ 𝐼 )
31 simplr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) ) → 𝑥 ∈ 𝑋 )
32 28 30 31 6 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) ) → 𝐴 ∈ ℂ )
33 snidg ⊢ ( 𝐸 ∈ V → 𝐸 ∈ { 𝐸 } )
34 8 33 syl ⊢ ( 𝜑 → 𝐸 ∈ { 𝐸 } )
35 elun2 ⊢ ( 𝐸 ∈ { 𝐸 } → 𝐸 ∈ ( 𝐷 ∪ { 𝐸 } ) )
36 34 35 syl ⊢ ( 𝜑 → 𝐸 ∈ ( 𝐷 ∪ { 𝐸 } ) )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐸 ∈ ( 𝐷 ∪ { 𝐸 } ) )
38 16 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 = 𝐸 ) → 𝐴 = 𝐹 )
39 21 22 27 32 37 38 fprodsplit1f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∏ 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) 𝐴 = ( 𝐹 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 ) )
40 difundir ⊢ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) = ( ( 𝐷 ∖ { 𝐸 } ) ∪ ( { 𝐸 } ∖ { 𝐸 } ) )
41 40 a1i ⊢ ( 𝜑 → ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) = ( ( 𝐷 ∖ { 𝐸 } ) ∪ ( { 𝐸 } ∖ { 𝐸 } ) ) )
42 difsn ⊢ ( ¬ 𝐸 ∈ 𝐷 → ( 𝐷 ∖ { 𝐸 } ) = 𝐷 )
43 9 42 syl ⊢ ( 𝜑 → ( 𝐷 ∖ { 𝐸 } ) = 𝐷 )
44 difid ⊢ ( { 𝐸 } ∖ { 𝐸 } ) = ∅
45 44 a1i ⊢ ( 𝜑 → ( { 𝐸 } ∖ { 𝐸 } ) = ∅ )
46 43 45 uneq12d ⊢ ( 𝜑 → ( ( 𝐷 ∖ { 𝐸 } ) ∪ ( { 𝐸 } ∖ { 𝐸 } ) ) = ( 𝐷 ∪ ∅ ) )
47 un0 ⊢ ( 𝐷 ∪ ∅ ) = 𝐷
48 47 a1i ⊢ ( 𝜑 → ( 𝐷 ∪ ∅ ) = 𝐷 )
49 41 46 48 3eqtrd ⊢ ( 𝜑 → ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) = 𝐷 )
50 49 prodeq1d ⊢ ( 𝜑 → ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 = ∏ 𝑖 ∈ 𝐷 𝐴 )
51 50 oveq2d ⊢ ( 𝜑 → ( 𝐹 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 ) = ( 𝐹 · ∏ 𝑖 ∈ 𝐷 𝐴 ) )
52 51 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐹 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 ) = ( 𝐹 · ∏ 𝑖 ∈ 𝐷 𝐴 ) )
53 39 52 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∏ 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) 𝐴 = ( 𝐹 · ∏ 𝑖 ∈ 𝐷 𝐴 ) )
54 1 53 mpteq2da ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 · ∏ 𝑖 ∈ 𝐷 𝐴 ) ) )
55 54 oveq2d ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 · ∏ 𝑖 ∈ 𝐷 𝐴 ) ) ) )
56 10 36 sseldd ⊢ ( 𝜑 → 𝐸 ∈ 𝐼 )
57 56 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐸 ∈ 𝐼 )
58 simpl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝜑 )
59 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
60 58 57 59 3jca ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) )
61 nfcv ⊢ Ⅎ 𝑖 𝐸
62 nfv ⊢ Ⅎ 𝑖 𝐸 ∈ 𝐼
63 2 62 20 nf3an ⊢ Ⅎ 𝑖 ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 )
64 nfcv ⊢ Ⅎ 𝑖 ℂ
65 4 64 nfel ⊢ Ⅎ 𝑖 𝐹 ∈ ℂ
66 63 65 nfim ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 ∈ ℂ )
67 ancom ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 = 𝐸 ) ↔ ( 𝑖 = 𝐸 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ) )
68 67 imbi1i ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 = 𝐸 ) → 𝐴 = 𝐹 ) ↔ ( ( 𝑖 = 𝐸 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐴 = 𝐹 ) )
69 eqcom ⊢ ( 𝐴 = 𝐹 ↔ 𝐹 = 𝐴 )
70 69 imbi2i ⊢ ( ( ( 𝑖 = 𝐸 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐴 = 𝐹 ) ↔ ( ( 𝑖 = 𝐸 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐹 = 𝐴 ) )
71 68 70 bitri ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 = 𝐸 ) → 𝐴 = 𝐹 ) ↔ ( ( 𝑖 = 𝐸 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐹 = 𝐴 ) )
72 38 71 mpbi ⊢ ( ( 𝑖 = 𝐸 ∧ ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐹 = 𝐴 )
73 72 3adantr2 ⊢ ( ( 𝑖 = 𝐸 ∧ ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐹 = 𝐴 )
74 73 3adant2 ⊢ ( ( 𝑖 = 𝐸 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) ∧ ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐹 = 𝐴 )
75 simp3 ⊢ ( ( 𝑖 = 𝐸 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) ∧ ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) → ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) )
76 eleq1 ⊢ ( 𝑖 = 𝐸 → ( 𝑖 ∈ 𝐼 ↔ 𝐸 ∈ 𝐼 ) )
77 76 3anbi2d ⊢ ( 𝑖 = 𝐸 → ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ↔ ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) )
78 77 imbi1d ⊢ ( 𝑖 = 𝐸 → ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) ) )
79 78 biimpa ⊢ ( ( 𝑖 = 𝐸 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) ) → ( ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) )
80 79 3adant3 ⊢ ( ( 𝑖 = 𝐸 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) ∧ ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) → ( ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) )
81 75 80 mpd ⊢ ( ( 𝑖 = 𝐸 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) ∧ ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐴 ∈ ℂ )
82 74 81 eqeltrd ⊢ ( ( 𝑖 = 𝐸 ∧ ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) ∧ ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) ) → 𝐹 ∈ ℂ )
83 82 3exp ⊢ ( 𝑖 = 𝐸 → ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) → ( ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 ∈ ℂ ) ) )
84 6 2a1i ⊢ ( 𝑖 = 𝐸 → ( ( ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 ∈ ℂ ) → ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) ) )
85 83 84 impbid ⊢ ( 𝑖 = 𝐸 → ( ( ( 𝜑 ∧ 𝑖 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 ∈ ℂ ) ) )
86 61 66 85 6 vtoclgf ⊢ ( 𝐸 ∈ 𝐼 → ( ( 𝜑 ∧ 𝐸 ∈ 𝐼 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 ∈ ℂ ) )
87 57 60 86 sylc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐹 ∈ ℂ )
88 58 7 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ Fin )
89 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ 𝐷 ) → 𝜑 )
90 10 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐷 ) → ( 𝐷 ∪ { 𝐸 } ) ⊆ 𝐼 )
91 elun1 ⊢ ( 𝑖 ∈ 𝐷 → 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) )
92 91 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐷 ) → 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) )
93 90 92 sseldd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ 𝐷 ) → 𝑖 ∈ 𝐼 )
94 93 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ 𝐷 ) → 𝑖 ∈ 𝐼 )
95 59 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ 𝐷 ) → 𝑥 ∈ 𝑋 )
96 89 94 95 6 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ 𝐷 ) → 𝐴 ∈ ℂ )
97 21 88 96 fprodclf ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∏ 𝑖 ∈ 𝐷 𝐴 ∈ ℂ )
98 nfv ⊢ Ⅎ 𝑗 𝑥 ∈ 𝑋
99 3 98 nfan ⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑥 ∈ 𝑋 )
100 diffi ⊢ ( 𝐷 ∈ Fin → ( 𝐷 ∖ { 𝑗 } ) ∈ Fin )
101 7 100 syl ⊢ ( 𝜑 → ( 𝐷 ∖ { 𝑗 } ) ∈ Fin )
102 101 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐷 ∖ { 𝑗 } ) ∈ Fin )
103 eldifi ⊢ ( 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) → 𝑖 ∈ 𝐷 )
104 103 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) ) → 𝑖 ∈ 𝐷 )
105 104 96 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) ) → 𝐴 ∈ ℂ )
106 21 102 105 fprodclf ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ∈ ℂ )
107 106 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ∈ ℂ )
108 12 107 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) ∈ ℂ )
109 99 88 108 fsumclf ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) ∈ ℂ )
110 1 11 87 14 15 97 109 13 dvmptmulf ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐹 · ∏ 𝑖 ∈ 𝐷 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐺 · ∏ 𝑖 ∈ 𝐷 𝐴 ) + ( Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) ) ) )
111 nfcv ⊢ Ⅎ 𝑗 ·
112 nfcv ⊢ Ⅎ 𝑗 ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴
113 5 111 112 nfov ⊢ Ⅎ 𝑗 ( 𝐺 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 )
114 58 8 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐸 ∈ V )
115 58 9 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ¬ 𝐸 ∈ 𝐷 )
116 diffi ⊢ ( ( 𝐷 ∪ { 𝐸 } ) ∈ Fin → ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) ∈ Fin )
117 26 116 syl ⊢ ( 𝜑 → ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) ∈ Fin )
118 117 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) ∈ Fin )
119 eldifi ⊢ ( 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) → 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) )
120 119 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) ) → 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) )
121 120 32 syldan ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) ) → 𝐴 ∈ ℂ )
122 21 118 121 fprodclf ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ∈ ℂ )
123 122 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ∈ ℂ )
124 12 123 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) ∈ ℂ )
125 sneq ⊢ ( 𝑗 = 𝐸 → { 𝑗 } = { 𝐸 } )
126 125 difeq2d ⊢ ( 𝑗 = 𝐸 → ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) = ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) )
127 126 prodeq1d ⊢ ( 𝑗 = 𝐸 → ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 = ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 )
128 17 127 oveq12d ⊢ ( 𝑗 = 𝐸 → ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) = ( 𝐺 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 ) )
129 49 7 eqeltrd ⊢ ( 𝜑 → ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) ∈ Fin )
130 129 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) ∈ Fin )
131 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) ) → 𝜑 )
132 10 adantr ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) ) → ( 𝐷 ∪ { 𝐸 } ) ⊆ 𝐼 )
133 eldifi ⊢ ( 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) → 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) )
134 133 adantl ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) ) → 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) )
135 132 134 sseldd ⊢ ( ( 𝜑 ∧ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) ) → 𝑖 ∈ 𝐼 )
136 135 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) ) → 𝑖 ∈ 𝐼 )
137 59 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) ) → 𝑥 ∈ 𝑋 )
138 131 136 137 6 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) ) → 𝐴 ∈ ℂ )
139 21 130 138 fprodclf ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 ∈ ℂ )
140 14 139 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 ) ∈ ℂ )
141 99 113 88 114 115 124 128 140 fsumsplitsn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Σ 𝑗 ∈ ( 𝐷 ∪ { 𝐸 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) = ( Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) + ( 𝐺 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 ) ) )
142 difundir ⊢ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) = ( ( 𝐷 ∖ { 𝑗 } ) ∪ ( { 𝐸 } ∖ { 𝑗 } ) )
143 142 a1i ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) → ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) = ( ( 𝐷 ∖ { 𝑗 } ) ∪ ( { 𝐸 } ∖ { 𝑗 } ) ) )
144 nfv ⊢ Ⅎ 𝑥 𝑗 ∈ 𝐷
145 1 144 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑗 ∈ 𝐷 )
146 elsni ⊢ ( 𝑥 ∈ { 𝐸 } → 𝑥 = 𝐸 )
147 146 eqcomd ⊢ ( 𝑥 ∈ { 𝐸 } → 𝐸 = 𝑥 )
148 147 adantr ⊢ ( ( 𝑥 ∈ { 𝐸 } ∧ 𝑥 = 𝑗 ) → 𝐸 = 𝑥 )
149 simpr ⊢ ( ( 𝑥 ∈ { 𝐸 } ∧ 𝑥 = 𝑗 ) → 𝑥 = 𝑗 )
150 eqidd ⊢ ( ( 𝑥 ∈ { 𝐸 } ∧ 𝑥 = 𝑗 ) → 𝑗 = 𝑗 )
151 148 149 150 3eqtrd ⊢ ( ( 𝑥 ∈ { 𝐸 } ∧ 𝑥 = 𝑗 ) → 𝐸 = 𝑗 )
152 151 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝐸 } ) ∧ 𝑥 = 𝑗 ) → 𝐸 = 𝑗 )
153 simpllr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝐸 } ) ∧ 𝑥 = 𝑗 ) → 𝑗 ∈ 𝐷 )
154 152 153 eqeltrd ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝐸 } ) ∧ 𝑥 = 𝑗 ) → 𝐸 ∈ 𝐷 )
155 9 ad3antrrr ⊢ ( ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝐸 } ) ∧ 𝑥 = 𝑗 ) → ¬ 𝐸 ∈ 𝐷 )
156 154 155 pm2.65da ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝐸 } ) → ¬ 𝑥 = 𝑗 )
157 velsn ⊢ ( 𝑥 ∈ { 𝑗 } ↔ 𝑥 = 𝑗 )
158 156 157 sylnibr ⊢ ( ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) ∧ 𝑥 ∈ { 𝐸 } ) → ¬ 𝑥 ∈ { 𝑗 } )
159 158 ex ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) → ( 𝑥 ∈ { 𝐸 } → ¬ 𝑥 ∈ { 𝑗 } ) )
160 145 159 ralrimi ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) → ∀ 𝑥 ∈ { 𝐸 } ¬ 𝑥 ∈ { 𝑗 } )
161 disj ⊢ ( ( { 𝐸 } ∩ { 𝑗 } ) = ∅ ↔ ∀ 𝑥 ∈ { 𝐸 } ¬ 𝑥 ∈ { 𝑗 } )
162 160 161 sylibr ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) → ( { 𝐸 } ∩ { 𝑗 } ) = ∅ )
163 disjdif2 ⊢ ( ( { 𝐸 } ∩ { 𝑗 } ) = ∅ → ( { 𝐸 } ∖ { 𝑗 } ) = { 𝐸 } )
164 162 163 syl ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) → ( { 𝐸 } ∖ { 𝑗 } ) = { 𝐸 } )
165 164 uneq2d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) → ( ( 𝐷 ∖ { 𝑗 } ) ∪ ( { 𝐸 } ∖ { 𝑗 } ) ) = ( ( 𝐷 ∖ { 𝑗 } ) ∪ { 𝐸 } ) )
166 143 165 eqtrd ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) → ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) = ( ( 𝐷 ∖ { 𝑗 } ) ∪ { 𝐸 } ) )
167 166 prodeq1d ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐷 ) → ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 = ∏ 𝑖 ∈ ( ( 𝐷 ∖ { 𝑗 } ) ∪ { 𝐸 } ) 𝐴 )
168 167 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 = ∏ 𝑖 ∈ ( ( 𝐷 ∖ { 𝑗 } ) ∪ { 𝐸 } ) 𝐴 )
169 nfv ⊢ Ⅎ 𝑖 𝑗 ∈ 𝐷
170 21 169 nfan ⊢ Ⅎ 𝑖 ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 )
171 102 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ( 𝐷 ∖ { 𝑗 } ) ∈ Fin )
172 58 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → 𝜑 )
173 172 8 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → 𝐸 ∈ V )
174 id ⊢ ( ¬ 𝐸 ∈ 𝐷 → ¬ 𝐸 ∈ 𝐷 )
175 174 intnanrd ⊢ ( ¬ 𝐸 ∈ 𝐷 → ¬ ( 𝐸 ∈ 𝐷 ∧ ¬ 𝐸 ∈ { 𝑗 } ) )
176 174 175 syl ⊢ ( ¬ 𝐸 ∈ 𝐷 → ¬ ( 𝐸 ∈ 𝐷 ∧ ¬ 𝐸 ∈ { 𝑗 } ) )
177 eldif ⊢ ( 𝐸 ∈ ( 𝐷 ∖ { 𝑗 } ) ↔ ( 𝐸 ∈ 𝐷 ∧ ¬ 𝐸 ∈ { 𝑗 } ) )
178 176 177 sylnibr ⊢ ( ¬ 𝐸 ∈ 𝐷 → ¬ 𝐸 ∈ ( 𝐷 ∖ { 𝑗 } ) )
179 9 178 syl ⊢ ( 𝜑 → ¬ 𝐸 ∈ ( 𝐷 ∖ { 𝑗 } ) )
180 172 179 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ¬ 𝐸 ∈ ( 𝐷 ∖ { 𝑗 } ) )
181 105 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) ∧ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) ) → 𝐴 ∈ ℂ )
182 87 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → 𝐹 ∈ ℂ )
183 170 4 171 173 180 181 16 182 fprodsplitsn ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ∏ 𝑖 ∈ ( ( 𝐷 ∖ { 𝑗 } ) ∪ { 𝐸 } ) 𝐴 = ( ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 · 𝐹 ) )
184 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ( ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 · 𝐹 ) = ( ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 · 𝐹 ) )
185 168 183 184 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 = ( ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 · 𝐹 ) )
186 185 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) = ( 𝐶 · ( ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 · 𝐹 ) ) )
187 12 107 182 mulassd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ( ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) = ( 𝐶 · ( ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 · 𝐹 ) ) )
188 187 eqcomd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ( 𝐶 · ( ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 · 𝐹 ) ) = ( ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) )
189 186 188 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ∧ 𝑗 ∈ 𝐷 ) → ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) = ( ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) )
190 189 ex ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑗 ∈ 𝐷 → ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) = ( ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) ) )
191 99 190 ralrimi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ∀ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) = ( ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) )
192 191 sumeq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) = Σ 𝑗 ∈ 𝐷 ( ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) )
193 99 88 87 108 fsummulc1f ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) = Σ 𝑗 ∈ 𝐷 ( ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) )
194 193 eqcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Σ 𝑗 ∈ 𝐷 ( ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) = ( Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) )
195 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) = ( Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) )
196 192 194 195 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) = ( Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) )
197 109 87 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) ∈ ℂ )
198 196 197 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) ∈ ℂ )
199 198 140 addcomd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) + ( 𝐺 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 ) ) = ( ( 𝐺 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 ) + Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) ) )
200 50 oveq2d ⊢ ( 𝜑 → ( 𝐺 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 ) = ( 𝐺 · ∏ 𝑖 ∈ 𝐷 𝐴 ) )
201 200 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( 𝐺 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 ) = ( 𝐺 · ∏ 𝑖 ∈ 𝐷 𝐴 ) )
202 201 196 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐺 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝐸 } ) 𝐴 ) + Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) ) = ( ( 𝐺 · ∏ 𝑖 ∈ 𝐷 𝐴 ) + ( Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) ) )
203 141 199 202 3eqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐺 · ∏ 𝑖 ∈ 𝐷 𝐴 ) + ( Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) ) = Σ 𝑗 ∈ ( 𝐷 ∪ { 𝐸 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) )
204 1 203 mpteq2da ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐺 · ∏ 𝑖 ∈ 𝐷 𝐴 ) + ( Σ 𝑗 ∈ 𝐷 ( 𝐶 · ∏ 𝑖 ∈ ( 𝐷 ∖ { 𝑗 } ) 𝐴 ) · 𝐹 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ ( 𝐷 ∪ { 𝐸 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) ) )
205 55 110 204 3eqtrd ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ∏ 𝑖 ∈ ( 𝐷 ∪ { 𝐸 } ) 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ Σ 𝑗 ∈ ( 𝐷 ∪ { 𝐸 } ) ( 𝐶 · ∏ 𝑖 ∈ ( ( 𝐷 ∪ { 𝐸 } ) ∖ { 𝑗 } ) 𝐴 ) ) )