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