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 ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
psrplusgpropd.b2 ( 𝜑𝐵 = ( Base ‘ 𝑆 ) )
psrplusgpropd.p ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝑅 ) 𝑦 ) = ( 𝑥 ( +g𝑆 ) 𝑦 ) )
Assertion psrplusgpropd ( 𝜑 → ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ ( 𝐼 mPwSer 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 psrplusgpropd.b1 ( 𝜑𝐵 = ( Base ‘ 𝑅 ) )
2 psrplusgpropd.b2 ( 𝜑𝐵 = ( Base ‘ 𝑆 ) )
3 psrplusgpropd.p ( ( 𝜑 ∧ ( 𝑥𝐵𝑦𝐵 ) ) → ( 𝑥 ( +g𝑅 ) 𝑦 ) = ( 𝑥 ( +g𝑆 ) 𝑦 ) )
4 simpl1 ( ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ) → 𝜑 )
5 eqid ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
6 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } = { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin }
8 eqid ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑅 ) )
9 simp2 ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
10 5 6 7 8 9 psrelbas ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑎 : { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
11 10 ffvelrnda ( ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ) → ( 𝑎𝑑 ) ∈ ( Base ‘ 𝑅 ) )
12 4 1 syl ( ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ) → 𝐵 = ( Base ‘ 𝑅 ) )
13 11 12 eleqtrrd ( ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ) → ( 𝑎𝑑 ) ∈ 𝐵 )
14 simp3 ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
15 5 6 7 8 14 psrelbas ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑏 : { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
16 15 ffvelrnda ( ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ) → ( 𝑏𝑑 ) ∈ ( Base ‘ 𝑅 ) )
17 16 12 eleqtrrd ( ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ) → ( 𝑏𝑑 ) ∈ 𝐵 )
18 3 oveqrspc2v ( ( 𝜑 ∧ ( ( 𝑎𝑑 ) ∈ 𝐵 ∧ ( 𝑏𝑑 ) ∈ 𝐵 ) ) → ( ( 𝑎𝑑 ) ( +g𝑅 ) ( 𝑏𝑑 ) ) = ( ( 𝑎𝑑 ) ( +g𝑆 ) ( 𝑏𝑑 ) ) )
19 4 13 17 18 syl12anc ( ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ) → ( ( 𝑎𝑑 ) ( +g𝑅 ) ( 𝑏𝑑 ) ) = ( ( 𝑎𝑑 ) ( +g𝑆 ) ( 𝑏𝑑 ) ) )
20 19 mpteq2dva ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ↦ ( ( 𝑎𝑑 ) ( +g𝑅 ) ( 𝑏𝑑 ) ) ) = ( 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ↦ ( ( 𝑎𝑑 ) ( +g𝑆 ) ( 𝑏𝑑 ) ) ) )
21 10 ffnd ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑎 Fn { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } )
22 15 ffnd ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑏 Fn { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } )
23 ovex ( ℕ0m 𝐼 ) ∈ V
24 23 rabex { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ∈ V
25 24 a1i ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ∈ V )
26 inidm ( { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ∩ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ) = { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin }
27 eqidd ( ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ) → ( 𝑎𝑑 ) = ( 𝑎𝑑 ) )
28 eqidd ( ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ) → ( 𝑏𝑑 ) = ( 𝑏𝑑 ) )
29 21 22 25 25 26 27 28 offval ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( 𝑎f ( +g𝑅 ) 𝑏 ) = ( 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ↦ ( ( 𝑎𝑑 ) ( +g𝑅 ) ( 𝑏𝑑 ) ) ) )
30 21 22 25 25 26 27 28 offval ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( 𝑎f ( +g𝑆 ) 𝑏 ) = ( 𝑑 ∈ { 𝑐 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑐 “ ℕ ) ∈ Fin } ↦ ( ( 𝑎𝑑 ) ( +g𝑆 ) ( 𝑏𝑑 ) ) ) )
31 20 29 30 3eqtr4d ( ( 𝜑𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( 𝑎f ( +g𝑅 ) 𝑏 ) = ( 𝑎f ( +g𝑆 ) 𝑏 ) )
32 31 mpoeq3dva ( 𝜑 → ( 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) , 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ↦ ( 𝑎f ( +g𝑅 ) 𝑏 ) ) = ( 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) , 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ↦ ( 𝑎f ( +g𝑆 ) 𝑏 ) ) )
33 1 2 eqtr3d ( 𝜑 → ( Base ‘ 𝑅 ) = ( Base ‘ 𝑆 ) )
34 33 psrbaspropd ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) )
35 mpoeq12 ( ( ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ∧ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ) → ( 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) , 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ↦ ( 𝑎f ( +g𝑆 ) 𝑏 ) ) = ( 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) , 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ↦ ( 𝑎f ( +g𝑆 ) 𝑏 ) ) )
36 34 34 35 syl2anc ( 𝜑 → ( 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) , 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ↦ ( 𝑎f ( +g𝑆 ) 𝑏 ) ) = ( 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) , 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ↦ ( 𝑎f ( +g𝑆 ) 𝑏 ) ) )
37 32 36 eqtrd ( 𝜑 → ( 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) , 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ↦ ( 𝑎f ( +g𝑅 ) 𝑏 ) ) = ( 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) , 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ↦ ( 𝑎f ( +g𝑆 ) 𝑏 ) ) )
38 ofmres ( ∘f ( +g𝑅 ) ↾ ( ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) × ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ) = ( 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) , 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ↦ ( 𝑎f ( +g𝑅 ) 𝑏 ) )
39 ofmres ( ∘f ( +g𝑆 ) ↾ ( ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) × ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ) ) = ( 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) , 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ↦ ( 𝑎f ( +g𝑆 ) 𝑏 ) )
40 37 38 39 3eqtr4g ( 𝜑 → ( ∘f ( +g𝑅 ) ↾ ( ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) × ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ) = ( ∘f ( +g𝑆 ) ↾ ( ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) × ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ) ) )
41 eqid ( +g𝑅 ) = ( +g𝑅 )
42 eqid ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ ( 𝐼 mPwSer 𝑅 ) )
43 5 8 41 42 psrplusg ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( ∘f ( +g𝑅 ) ↾ ( ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) × ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) )
44 eqid ( 𝐼 mPwSer 𝑆 ) = ( 𝐼 mPwSer 𝑆 )
45 eqid ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) )
46 eqid ( +g𝑆 ) = ( +g𝑆 )
47 eqid ( +g ‘ ( 𝐼 mPwSer 𝑆 ) ) = ( +g ‘ ( 𝐼 mPwSer 𝑆 ) )
48 44 45 46 47 psrplusg ( +g ‘ ( 𝐼 mPwSer 𝑆 ) ) = ( ∘f ( +g𝑆 ) ↾ ( ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) × ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ) )
49 40 43 48 3eqtr4g ( 𝜑 → ( +g ‘ ( 𝐼 mPwSer 𝑅 ) ) = ( +g ‘ ( 𝐼 mPwSer 𝑆 ) ) )