Metamath Proof Explorer

Theorem psrplusgpropd

Description: Property deduction for power series addition. (Contributed by Stefan O'Rear, 27-Mar-2015) (Revised by Mario Carneiro, 3-Oct-2015)

Ref Expression
Hypotheses psrplusgpropd.b1 ⊢ φ → B = Base R
psrplusgpropd.b2 ⊢ φ → B = Base S
psrplusgpropd.p ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + R y = x + S y
Assertion psrplusgpropd ⊢ φ → + I mPwSer R = + I mPwSer S

Proof

Step Hyp Ref Expression
1 psrplusgpropd.b1 ⊢ φ → B = Base R
2 psrplusgpropd.b2 ⊢ φ → B = Base S
3 psrplusgpropd.p ⊢ φ ∧ x ∈ B ∧ y ∈ B → x + R y = x + S y
4 simpl1 ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R ∧ d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin → φ
5 eqid ⊢ I mPwSer R = I mPwSer R
6 eqid ⊢ Base R = Base R
7 eqid ⊢ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin = c ∈ ℕ 0 I | c -1 ℕ ∈ Fin
8 eqid ⊢ Base I mPwSer R = Base I mPwSer R
9 simp2 ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R → a ∈ Base I mPwSer R
10 5 6 7 8 9 psrelbas ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R → a : c ∈ ℕ 0 I | c -1 ℕ ∈ Fin ⟶ Base R
11 10 ffvelrnda ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R ∧ d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin → a ⁡ d ∈ Base R
12 4 1 syl ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R ∧ d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin → B = Base R
13 11 12 eleqtrrd ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R ∧ d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin → a ⁡ d ∈ B
14 simp3 ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R → b ∈ Base I mPwSer R
15 5 6 7 8 14 psrelbas ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R → b : c ∈ ℕ 0 I | c -1 ℕ ∈ Fin ⟶ Base R
16 15 ffvelrnda ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R ∧ d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin → b ⁡ d ∈ Base R
17 16 12 eleqtrrd ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R ∧ d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin → b ⁡ d ∈ B
18 3 oveqrspc2v ⊢ φ ∧ a ⁡ d ∈ B ∧ b ⁡ d ∈ B → a ⁡ d + R b ⁡ d = a ⁡ d + S b ⁡ d
19 4 13 17 18 syl12anc ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R ∧ d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin → a ⁡ d + R b ⁡ d = a ⁡ d + S b ⁡ d
20 19 mpteq2dva ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R → d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin ⟼ a ⁡ d + R b ⁡ d = d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin ⟼ a ⁡ d + S b ⁡ d
21 10 ffnd ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R → a Fn c ∈ ℕ 0 I | c -1 ℕ ∈ Fin
22 15 ffnd ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R → b Fn c ∈ ℕ 0 I | c -1 ℕ ∈ Fin
23 ovex ⊢ ℕ 0 I ∈ V
24 23 rabex ⊢ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin ∈ V
25 24 a1i ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R → c ∈ ℕ 0 I | c -1 ℕ ∈ Fin ∈ V
26 inidm ⊢ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin ∩ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin = c ∈ ℕ 0 I | c -1 ℕ ∈ Fin
27 eqidd ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R ∧ d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin → a ⁡ d = a ⁡ d
28 eqidd ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R ∧ d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin → b ⁡ d = b ⁡ d
29 21 22 25 25 26 27 28 offval ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R → a + R f b = d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin ⟼ a ⁡ d + R b ⁡ d
30 21 22 25 25 26 27 28 offval ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R → a + S f b = d ∈ c ∈ ℕ 0 I | c -1 ℕ ∈ Fin ⟼ a ⁡ d + S b ⁡ d
31 20 29 30 3eqtr4d ⊢ φ ∧ a ∈ Base I mPwSer R ∧ b ∈ Base I mPwSer R → a + R f b = a + S f b
32 31 mpoeq3dva ⊢ φ → a ∈ Base I mPwSer R , b ∈ Base I mPwSer R ⟼ a + R f b = a ∈ Base I mPwSer R , b ∈ Base I mPwSer R ⟼ a + S f b
33 1 2 eqtr3d ⊢ φ → Base R = Base S
34 33 psrbaspropd ⊢ φ → Base I mPwSer R = Base I mPwSer S
35 mpoeq12 ⊢ Base I mPwSer R = Base I mPwSer S ∧ Base I mPwSer R = Base I mPwSer S → a ∈ Base I mPwSer R , b ∈ Base I mPwSer R ⟼ a + S f b = a ∈ Base I mPwSer S , b ∈ Base I mPwSer S ⟼ a + S f b
36 34 34 35 syl2anc ⊢ φ → a ∈ Base I mPwSer R , b ∈ Base I mPwSer R ⟼ a + S f b = a ∈ Base I mPwSer S , b ∈ Base I mPwSer S ⟼ a + S f b
37 32 36 eqtrd ⊢ φ → a ∈ Base I mPwSer R , b ∈ Base I mPwSer R ⟼ a + R f b = a ∈ Base I mPwSer S , b ∈ Base I mPwSer S ⟼ a + S f b
38 ofmres ⊢ ∘ f ⁡ + R ↾ Base I mPwSer R × Base I mPwSer R = a ∈ Base I mPwSer R , b ∈ Base I mPwSer R ⟼ a + R f b
39 ofmres ⊢ ∘ f ⁡ + S ↾ Base I mPwSer S × Base I mPwSer S = a ∈ Base I mPwSer S , b ∈ Base I mPwSer S ⟼ a + S f b
40 37 38 39 3eqtr4g ⊢ φ → ∘ f ⁡ + R ↾ Base I mPwSer R × Base I mPwSer R = ∘ f ⁡ + S ↾ Base I mPwSer S × Base I mPwSer S
41 eqid ⊢ + R = + R
42 eqid ⊢ + I mPwSer R = + I mPwSer R
43 5 8 41 42 psrplusg ⊢ + I mPwSer R = ∘ f ⁡ + R ↾ Base I mPwSer R × Base I mPwSer R
44 eqid ⊢ I mPwSer S = I mPwSer S
45 eqid ⊢ Base I mPwSer S = Base I mPwSer S
46 eqid ⊢ + S = + S
47 eqid ⊢ + I mPwSer S = + I mPwSer S
48 44 45 46 47 psrplusg ⊢ + I mPwSer S = ∘ f ⁡ + S ↾ Base I mPwSer S × Base I mPwSer S
49 40 43 48 3eqtr4g ⊢ φ → + I mPwSer R = + I mPwSer S