Metamath Proof Explorer

Theorem psdadd

Description: The derivative of a sum is the sum of the derivatives. (Contributed by SN, 12-Apr-2025)

Ref Expression
Hypotheses psdadd.s ⊢ S = I mPwSer R
psdadd.b ⊢ B = Base S
psdadd.p ⊢ + ˙ = + S
psdadd.i ⊢ φ → I ∈ V
psdadd.r ⊢ φ → R ∈ CMnd
psdadd.x ⊢ φ → X ∈ I
psdadd.f ⊢ φ → F ∈ B
psdadd.g ⊢ φ → G ∈ B
Assertion psdadd ⊢ φ → I mPSDer R ⁡ X ⁡ F + ˙ G = I mPSDer R ⁡ X ⁡ F + ˙ I mPSDer R ⁡ X ⁡ G

Proof

Step Hyp Ref Expression
1 psdadd.s ⊢ S = I mPwSer R
2 psdadd.b ⊢ B = Base S
3 psdadd.p ⊢ + ˙ = + S
4 psdadd.i ⊢ φ → I ∈ V
5 psdadd.r ⊢ φ → R ∈ CMnd
6 psdadd.x ⊢ φ → X ∈ I
7 psdadd.f ⊢ φ → F ∈ B
8 psdadd.g ⊢ φ → G ∈ B
9 eqid ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
10 1 2 9 4 5 6 7 psdval ⊢ φ → I mPSDer R ⁡ X ⁡ F = b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R F ⁡ b + f y ∈ I ⟼ if y = X 1 0
11 1 2 9 4 5 6 8 psdval ⊢ φ → I mPSDer R ⁡ X ⁡ G = b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R G ⁡ b + f y ∈ I ⟼ if y = X 1 0
12 10 11 oveq12d ⊢ φ → I mPSDer R ⁡ X ⁡ F + R f I mPSDer R ⁡ X ⁡ G = b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R F ⁡ b + f y ∈ I ⟼ if y = X 1 0 + R f b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R G ⁡ b + f y ∈ I ⟼ if y = X 1 0
13 ovex ⊢ b ⁡ X + 1 ⋅ R F ⁡ b + f y ∈ I ⟼ if y = X 1 0 ∈ V
14 eqid ⊢ b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R F ⁡ b + f y ∈ I ⟼ if y = X 1 0 = b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R F ⁡ b + f y ∈ I ⟼ if y = X 1 0
15 13 14 fnmpti ⊢ b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R F ⁡ b + f y ∈ I ⟼ if y = X 1 0 Fn h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
16 15 a1i ⊢ φ → b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R F ⁡ b + f y ∈ I ⟼ if y = X 1 0 Fn h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
17 ovex ⊢ b ⁡ X + 1 ⋅ R G ⁡ b + f y ∈ I ⟼ if y = X 1 0 ∈ V
18 eqid ⊢ b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R G ⁡ b + f y ∈ I ⟼ if y = X 1 0 = b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R G ⁡ b + f y ∈ I ⟼ if y = X 1 0
19 17 18 fnmpti ⊢ b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R G ⁡ b + f y ∈ I ⟼ if y = X 1 0 Fn h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
20 19 a1i ⊢ φ → b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R G ⁡ b + f y ∈ I ⟼ if y = X 1 0 Fn h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
21 ovex ⊢ ℕ 0 I ∈ V
22 21 rabex ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∈ V
23 22 a1i ⊢ φ → h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∈ V
24 inidm ⊢ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∩ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin = h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
25 fveq1 ⊢ b = d → b ⁡ X = d ⁡ X
26 25 oveq1d ⊢ b = d → b ⁡ X + 1 = d ⁡ X + 1
27 fvoveq1 ⊢ b = d → F ⁡ b + f y ∈ I ⟼ if y = X 1 0 = F ⁡ d + f y ∈ I ⟼ if y = X 1 0
28 26 27 oveq12d ⊢ b = d → b ⁡ X + 1 ⋅ R F ⁡ b + f y ∈ I ⟼ if y = X 1 0 = d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0
29 simpr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
30 ovexd ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0 ∈ V
31 14 28 29 30 fvmptd3 ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R F ⁡ b + f y ∈ I ⟼ if y = X 1 0 ⁡ d = d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0
32 fvoveq1 ⊢ b = d → G ⁡ b + f y ∈ I ⟼ if y = X 1 0 = G ⁡ d + f y ∈ I ⟼ if y = X 1 0
33 26 32 oveq12d ⊢ b = d → b ⁡ X + 1 ⋅ R G ⁡ b + f y ∈ I ⟼ if y = X 1 0 = d ⁡ X + 1 ⋅ R G ⁡ d + f y ∈ I ⟼ if y = X 1 0
34 ovexd ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X + 1 ⋅ R G ⁡ d + f y ∈ I ⟼ if y = X 1 0 ∈ V
35 18 33 29 34 fvmptd3 ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R G ⁡ b + f y ∈ I ⟼ if y = X 1 0 ⁡ d = d ⁡ X + 1 ⋅ R G ⁡ d + f y ∈ I ⟼ if y = X 1 0
36 16 20 23 23 24 31 35 offval ⊢ φ → b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R F ⁡ b + f y ∈ I ⟼ if y = X 1 0 + R f b ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ b ⁡ X + 1 ⋅ R G ⁡ b + f y ∈ I ⟼ if y = X 1 0 = d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0 + R d ⁡ X + 1 ⋅ R G ⁡ d + f y ∈ I ⟼ if y = X 1 0
37 eqid ⊢ + R = + R
38 1 2 37 3 7 8 psradd ⊢ φ → F + ˙ G = F + R f G
39 38 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F + ˙ G = F + R f G
40 39 fveq1d ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F + ˙ G ⁡ d + f y ∈ I ⟼ if y = X 1 0 = F + R f G ⁡ d + f y ∈ I ⟼ if y = X 1 0
41 9 psrbagsn ⊢ I ∈ V → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
42 4 41 syl ⊢ φ → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
43 42 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
44 9 psrbagaddcl ⊢ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ∧ y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
45 29 43 44 syl2anc ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
46 eqid ⊢ Base R = Base R
47 1 46 9 2 7 psrelbas ⊢ φ → F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
48 47 ffnd ⊢ φ → F Fn h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
49 1 46 9 2 8 psrelbas ⊢ φ → G : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
50 49 ffnd ⊢ φ → G Fn h ∈ ℕ 0 I | h -1 ℕ ∈ Fin
51 eqidd ⊢ φ ∧ d + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F ⁡ d + f y ∈ I ⟼ if y = X 1 0 = F ⁡ d + f y ∈ I ⟼ if y = X 1 0
52 eqidd ⊢ φ ∧ d + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → G ⁡ d + f y ∈ I ⟼ if y = X 1 0 = G ⁡ d + f y ∈ I ⟼ if y = X 1 0
53 48 50 23 23 24 51 52 ofval ⊢ φ ∧ d + f y ∈ I ⟼ if y = X 1 0 ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F + R f G ⁡ d + f y ∈ I ⟼ if y = X 1 0 = F ⁡ d + f y ∈ I ⟼ if y = X 1 0 + R G ⁡ d + f y ∈ I ⟼ if y = X 1 0
54 45 53 syldan ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F + R f G ⁡ d + f y ∈ I ⟼ if y = X 1 0 = F ⁡ d + f y ∈ I ⟼ if y = X 1 0 + R G ⁡ d + f y ∈ I ⟼ if y = X 1 0
55 40 54 eqtrd ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F + ˙ G ⁡ d + f y ∈ I ⟼ if y = X 1 0 = F ⁡ d + f y ∈ I ⟼ if y = X 1 0 + R G ⁡ d + f y ∈ I ⟼ if y = X 1 0
56 55 oveq2d ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X + 1 ⋅ R F + ˙ G ⁡ d + f y ∈ I ⟼ if y = X 1 0 = d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0 + R G ⁡ d + f y ∈ I ⟼ if y = X 1 0
57 5 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → R ∈ CMnd
58 9 psrbagf ⊢ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d : I ⟶ ℕ 0
59 58 adantl ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d : I ⟶ ℕ 0
60 6 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → X ∈ I
61 59 60 ffvelcdmd ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X ∈ ℕ 0
62 peano2nn0 ⊢ d ⁡ X ∈ ℕ 0 → d ⁡ X + 1 ∈ ℕ 0
63 61 62 syl ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X + 1 ∈ ℕ 0
64 7 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F ∈ B
65 1 46 9 2 64 psrelbas ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
66 65 45 ffvelcdmd ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → F ⁡ d + f y ∈ I ⟼ if y = X 1 0 ∈ Base R
67 49 adantr ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → G : h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟶ Base R
68 67 45 ffvelcdmd ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → G ⁡ d + f y ∈ I ⟼ if y = X 1 0 ∈ Base R
69 eqid ⊢ ⋅ R = ⋅ R
70 46 69 37 mulgnn0di ⊢ R ∈ CMnd ∧ d ⁡ X + 1 ∈ ℕ 0 ∧ F ⁡ d + f y ∈ I ⟼ if y = X 1 0 ∈ Base R ∧ G ⁡ d + f y ∈ I ⟼ if y = X 1 0 ∈ Base R → d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0 + R G ⁡ d + f y ∈ I ⟼ if y = X 1 0 = d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0 + R d ⁡ X + 1 ⋅ R G ⁡ d + f y ∈ I ⟼ if y = X 1 0
71 57 63 66 68 70 syl13anc ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0 + R G ⁡ d + f y ∈ I ⟼ if y = X 1 0 = d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0 + R d ⁡ X + 1 ⋅ R G ⁡ d + f y ∈ I ⟼ if y = X 1 0
72 56 71 eqtr2d ⊢ φ ∧ d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin → d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0 + R d ⁡ X + 1 ⋅ R G ⁡ d + f y ∈ I ⟼ if y = X 1 0 = d ⁡ X + 1 ⋅ R F + ˙ G ⁡ d + f y ∈ I ⟼ if y = X 1 0
73 72 mpteq2dva ⊢ φ → d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ d ⁡ X + 1 ⋅ R F ⁡ d + f y ∈ I ⟼ if y = X 1 0 + R d ⁡ X + 1 ⋅ R G ⁡ d + f y ∈ I ⟼ if y = X 1 0 = d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ d ⁡ X + 1 ⋅ R F + ˙ G ⁡ d + f y ∈ I ⟼ if y = X 1 0
74 12 36 73 3eqtrd ⊢ φ → I mPSDer R ⁡ X ⁡ F + R f I mPSDer R ⁡ X ⁡ G = d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ d ⁡ X + 1 ⋅ R F + ˙ G ⁡ d + f y ∈ I ⟼ if y = X 1 0
75 5 cmnmndd ⊢ φ → R ∈ Mnd
76 mndmgm ⊢ R ∈ Mnd → R ∈ Mgm
77 75 76 syl ⊢ φ → R ∈ Mgm
78 1 2 4 77 6 7 psdcl ⊢ φ → I mPSDer R ⁡ X ⁡ F ∈ B
79 1 2 4 77 6 8 psdcl ⊢ φ → I mPSDer R ⁡ X ⁡ G ∈ B
80 1 2 37 3 78 79 psradd ⊢ φ → I mPSDer R ⁡ X ⁡ F + ˙ I mPSDer R ⁡ X ⁡ G = I mPSDer R ⁡ X ⁡ F + R f I mPSDer R ⁡ X ⁡ G
81 1 2 3 77 7 8 psraddcl ⊢ φ → F + ˙ G ∈ B
82 1 2 9 4 5 6 81 psdval ⊢ φ → I mPSDer R ⁡ X ⁡ F + ˙ G = d ∈ h ∈ ℕ 0 I | h -1 ℕ ∈ Fin ⟼ d ⁡ X + 1 ⋅ R F + ˙ G ⁡ d + f y ∈ I ⟼ if y = X 1 0
83 74 80 82 3eqtr4rd ⊢ φ → I mPSDer R ⁡ X ⁡ F + ˙ G = I mPSDer R ⁡ X ⁡ F + ˙ I mPSDer R ⁡ X ⁡ G