Metamath Proof Explorer

Theorem dvmptmulf

Description: Function-builder for derivative, product rule. A version of dvmptmul using bound-variable hypotheses instead of distinct variable conditions. (Contributed by Glauco Siliprandi, 5-Apr-2020)

Ref Expression
Hypotheses dvmptmulf.ph ⊢ Ⅎ 𝑥 𝜑
dvmptmulf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
dvmptmulf.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
dvmptmulf.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
dvmptmulf.ab ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
dvmptmulf.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
dvmptmulf.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ 𝑊 )
dvmptmulf.cd ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
Assertion dvmptmulf ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 dvmptmulf.ph ⊢ Ⅎ 𝑥 𝜑
2 dvmptmulf.s ⊢ ( 𝜑 → 𝑆 ∈ { ℝ , ℂ } )
3 dvmptmulf.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ )
4 dvmptmulf.b ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 )
5 dvmptmulf.ab ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) )
6 dvmptmulf.c ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ )
7 dvmptmulf.d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ 𝑊 )
8 dvmptmulf.cd ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) = ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) )
9 nfcv ⊢ Ⅎ 𝑦 ( 𝐴 · 𝐶 )
10 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴
11 nfcv ⊢ Ⅎ 𝑥 ·
12 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶
13 10 11 12 nfov ⊢ Ⅎ 𝑥 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
14 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐴 = ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
15 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
16 14 15 oveq12d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 · 𝐶 ) = ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
17 9 13 16 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐶 ) ) = ( 𝑦 ∈ 𝑋 ↦ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
18 17 oveq2i ⊢ ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐶 ) ) ) = ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) )
19 18 a1i ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐶 ) ) ) = ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ) )
20 nfv ⊢ Ⅎ 𝑥 𝑦 ∈ 𝑋
21 1 20 nfan ⊢ Ⅎ 𝑥 ( 𝜑 ∧ 𝑦 ∈ 𝑋 )
22 10 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ
23 21 22 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ )
24 eleq1w ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ∈ 𝑋 ↔ 𝑦 ∈ 𝑋 ) )
25 24 anbi2d ⊢ ( 𝑥 = 𝑦 → ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) ↔ ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) ) )
26 14 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ∈ ℂ ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ ) )
27 25 26 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐴 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ ) ) )
28 23 27 3 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ∈ ℂ )
29 nfcv ⊢ Ⅎ 𝑥 𝑦
30 29 nfcsb1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵
31 nfcv ⊢ Ⅎ 𝑥 𝑉
32 30 31 nfel ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉
33 21 32 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
34 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
35 34 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐵 ∈ 𝑉 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) )
36 25 35 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐵 ∈ 𝑉 ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉 ) ) )
37 33 36 4 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ∈ 𝑉 )
38 nfcv ⊢ Ⅎ 𝑦 𝐴
39 csbeq1a ⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑥 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
40 csbcow ⊢ ⦋ 𝑥 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = ⦋ 𝑥 / 𝑥 ⦌ 𝐴
41 csbid ⊢ ⦋ 𝑥 / 𝑥 ⦌ 𝐴 = 𝐴
42 40 41 eqtri ⊢ ⦋ 𝑥 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐴
43 42 a1i ⊢ ( 𝑦 = 𝑥 → ⦋ 𝑥 / 𝑦 ⦌ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐴 )
44 39 43 eqtrd ⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐴 = 𝐴 )
45 10 38 44 cbvmpt ⊢ ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐴 )
46 45 oveq2i ⊢ ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) )
47 46 a1i ⊢ ( 𝜑 → ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐴 ) ) )
48 nfcv ⊢ Ⅎ 𝑦 𝐵
49 48 30 34 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 )
50 49 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐵 ) = ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
51 47 5 50 3eqtrd ⊢ ( 𝜑 → ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
52 12 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ℂ
53 21 52 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ℂ )
54 15 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐶 ∈ ℂ ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ℂ ) )
55 25 54 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐶 ∈ ℂ ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ℂ ) ) )
56 53 55 6 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ∈ ℂ )
57 29 nfcsb1 ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐷
58 nfcv ⊢ Ⅎ 𝑥 𝑊
59 57 58 nfel ⊢ Ⅎ 𝑥 ⦋ 𝑦 / 𝑥 ⦌ 𝐷 ∈ 𝑊
60 21 59 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐷 ∈ 𝑊 )
61 csbeq1a ⊢ ( 𝑥 = 𝑦 → 𝐷 = ⦋ 𝑦 / 𝑥 ⦌ 𝐷 )
62 61 eleq1d ⊢ ( 𝑥 = 𝑦 → ( 𝐷 ∈ 𝑊 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐷 ∈ 𝑊 ) )
63 25 62 imbi12d ⊢ ( 𝑥 = 𝑦 → ( ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ 𝑊 ) ↔ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐷 ∈ 𝑊 ) ) )
64 60 63 7 chvarfv ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑋 ) → ⦋ 𝑦 / 𝑥 ⦌ 𝐷 ∈ 𝑊 )
65 nfcv ⊢ Ⅎ 𝑦 𝐶
66 eqcom ⊢ ( 𝑥 = 𝑦 ↔ 𝑦 = 𝑥 )
67 66 imbi1i ⊢ ( ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ↔ ( 𝑦 = 𝑥 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) )
68 eqcom ⊢ ( 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = 𝐶 )
69 68 imbi2i ⊢ ( ( 𝑦 = 𝑥 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ↔ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = 𝐶 ) )
70 67 69 bitri ⊢ ( ( 𝑥 = 𝑦 → 𝐶 = ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ↔ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = 𝐶 ) )
71 15 70 mpbi ⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐶 = 𝐶 )
72 12 65 71 cbvmpt ⊢ ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) = ( 𝑥 ∈ 𝑋 ↦ 𝐶 )
73 72 oveq2i ⊢ ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) )
74 73 a1i ⊢ ( 𝜑 → ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) = ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ 𝐶 ) ) )
75 nfcv ⊢ Ⅎ 𝑦 𝐷
76 75 57 61 cbvmpt ⊢ ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) = ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐷 )
77 76 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 ↦ 𝐷 ) = ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐷 ) )
78 74 8 77 3eqtrd ⊢ ( 𝜑 → ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) = ( 𝑦 ∈ 𝑋 ↦ ⦋ 𝑦 / 𝑥 ⦌ 𝐷 ) )
79 2 28 37 51 56 64 78 dvmptmul ⊢ ( 𝜑 → ( 𝑆 D ( 𝑦 ∈ 𝑋 ↦ ( ⦋ 𝑦 / 𝑥 ⦌ 𝐴 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) ) ) = ( 𝑦 ∈ 𝑋 ↦ ( ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) + ( ⦋ 𝑦 / 𝑥 ⦌ 𝐷 · ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) ) )
80 30 11 12 nfov ⊢ Ⅎ 𝑥 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 )
81 nfcv ⊢ Ⅎ 𝑥 +
82 57 11 10 nfov ⊢ Ⅎ 𝑥 ( ⦋ 𝑦 / 𝑥 ⦌ 𝐷 · ⦋ 𝑦 / 𝑥 ⦌ 𝐴 )
83 80 81 82 nfov ⊢ Ⅎ 𝑥 ( ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) + ( ⦋ 𝑦 / 𝑥 ⦌ 𝐷 · ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) )
84 nfcv ⊢ Ⅎ 𝑦 ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) )
85 66 imbi1i ⊢ ( ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑦 = 𝑥 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) )
86 eqcom ⊢ ( 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 )
87 86 imbi2i ⊢ ( ( 𝑦 = 𝑥 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 ) )
88 85 87 bitri ⊢ ( ( 𝑥 = 𝑦 → 𝐵 = ⦋ 𝑦 / 𝑥 ⦌ 𝐵 ) ↔ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 ) )
89 34 88 mpbi ⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐵 = 𝐵 )
90 89 71 oveq12d ⊢ ( 𝑦 = 𝑥 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) = ( 𝐵 · 𝐶 ) )
91 66 imbi1i ⊢ ( ( 𝑥 = 𝑦 → 𝐷 = ⦋ 𝑦 / 𝑥 ⦌ 𝐷 ) ↔ ( 𝑦 = 𝑥 → 𝐷 = ⦋ 𝑦 / 𝑥 ⦌ 𝐷 ) )
92 eqcom ⊢ ( 𝐷 = ⦋ 𝑦 / 𝑥 ⦌ 𝐷 ↔ ⦋ 𝑦 / 𝑥 ⦌ 𝐷 = 𝐷 )
93 92 imbi2i ⊢ ( ( 𝑦 = 𝑥 → 𝐷 = ⦋ 𝑦 / 𝑥 ⦌ 𝐷 ) ↔ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐷 = 𝐷 ) )
94 91 93 bitri ⊢ ( ( 𝑥 = 𝑦 → 𝐷 = ⦋ 𝑦 / 𝑥 ⦌ 𝐷 ) ↔ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐷 = 𝐷 ) )
95 61 94 mpbi ⊢ ( 𝑦 = 𝑥 → ⦋ 𝑦 / 𝑥 ⦌ 𝐷 = 𝐷 )
96 95 44 oveq12d ⊢ ( 𝑦 = 𝑥 → ( ⦋ 𝑦 / 𝑥 ⦌ 𝐷 · ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) = ( 𝐷 · 𝐴 ) )
97 90 96 oveq12d ⊢ ( 𝑦 = 𝑥 → ( ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) + ( ⦋ 𝑦 / 𝑥 ⦌ 𝐷 · ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) = ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) )
98 83 84 97 cbvmpt ⊢ ( 𝑦 ∈ 𝑋 ↦ ( ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) + ( ⦋ 𝑦 / 𝑥 ⦌ 𝐷 · ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) )
99 98 a1i ⊢ ( 𝜑 → ( 𝑦 ∈ 𝑋 ↦ ( ( ⦋ 𝑦 / 𝑥 ⦌ 𝐵 · ⦋ 𝑦 / 𝑥 ⦌ 𝐶 ) + ( ⦋ 𝑦 / 𝑥 ⦌ 𝐷 · ⦋ 𝑦 / 𝑥 ⦌ 𝐴 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) ) )
100 19 79 99 3eqtrd ⊢ ( 𝜑 → ( 𝑆 D ( 𝑥 ∈ 𝑋 ↦ ( 𝐴 · 𝐶 ) ) ) = ( 𝑥 ∈ 𝑋 ↦ ( ( 𝐵 · 𝐶 ) + ( 𝐷 · 𝐴 ) ) ) )