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 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ) → 𝜑 )
5 eqid ⊢ ( 𝐼 mPwSer 𝑅 ) = ( 𝐼 mPwSer 𝑅 )
6 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
7 eqid ⊢ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } = { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ 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 𝑅 ) ) ) → 𝑎 : { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
11 10 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ) → ( 𝑎 ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
12 4 1 syl ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ) → 𝐵 = ( Base ‘ 𝑅 ) )
13 11 12 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ) → ( 𝑎 ‘ 𝑑 ) ∈ 𝐵 )
14 simp3 ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) )
15 5 6 7 8 14 psrelbas ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑏 : { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
16 15 ffvelrnda ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ) → ( 𝑏 ‘ 𝑑 ) ∈ ( Base ‘ 𝑅 ) )
17 16 12 eleqtrrd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ) → ( 𝑏 ‘ 𝑑 ) ∈ 𝐵 )
18 3 oveqrspc2v ⊢ ( ( 𝜑 ∧ ( ( 𝑎 ‘ 𝑑 ) ∈ 𝐵 ∧ ( 𝑏 ‘ 𝑑 ) ∈ 𝐵 ) ) → ( ( 𝑎 ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( 𝑏 ‘ 𝑑 ) ) = ( ( 𝑎 ‘ 𝑑 ) ( +g ‘ 𝑆 ) ( 𝑏 ‘ 𝑑 ) ) )
19 4 13 17 18 syl12anc ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ) → ( ( 𝑎 ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( 𝑏 ‘ 𝑑 ) ) = ( ( 𝑎 ‘ 𝑑 ) ( +g ‘ 𝑆 ) ( 𝑏 ‘ 𝑑 ) ) )
20 19 mpteq2dva ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ↦ ( ( 𝑎 ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( 𝑏 ‘ 𝑑 ) ) ) = ( 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ↦ ( ( 𝑎 ‘ 𝑑 ) ( +g ‘ 𝑆 ) ( 𝑏 ‘ 𝑑 ) ) ) )
21 10 ffnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑎 Fn { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } )
22 15 ffnd ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → 𝑏 Fn { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } )
23 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
24 23 rabex ⊢ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ∈ V
25 24 a1i ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ∈ V )
26 inidm ⊢ ( { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ∩ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ) = { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin }
27 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ) → ( 𝑎 ‘ 𝑑 ) = ( 𝑎 ‘ 𝑑 ) )
28 eqidd ⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) ∧ 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ) → ( 𝑏 ‘ 𝑑 ) = ( 𝑏 ‘ 𝑑 ) )
29 21 22 25 25 26 27 28 offval ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( 𝑎 ∘f ( +g ‘ 𝑅 ) 𝑏 ) = ( 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ Fin } ↦ ( ( 𝑎 ‘ 𝑑 ) ( +g ‘ 𝑅 ) ( 𝑏 ‘ 𝑑 ) ) ) )
30 21 22 25 25 26 27 28 offval ⊢ ( ( 𝜑 ∧ 𝑎 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ∧ 𝑏 ∈ ( Base ‘ ( 𝐼 mPwSer 𝑅 ) ) ) → ( 𝑎 ∘f ( +g ‘ 𝑆 ) 𝑏 ) = ( 𝑑 ∈ { 𝑐 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑐 “ ℕ ) ∈ 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 𝑆 ) ) )