Metamath Proof Explorer

Theorem psrgrp

Description: The ring of power series is a group. (Contributed by Mario Carneiro, 29-Dec-2014) (Proof shortened by SN, 7-Feb-2025)

Ref Expression
Hypotheses psrgrp.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
psrgrp.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
psrgrp.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
Assertion psrgrp ( 𝜑 → 𝑆 ∈ Grp )

Proof

Step Hyp Ref Expression
1 psrgrp.s ⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2 psrgrp.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
3 psrgrp.r ⊢ ( 𝜑 → 𝑅 ∈ Grp )
4 ovex ⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
5 4 rabex ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V
6 eqid ⊢ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) = ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } )
7 6 pwsgrp ⊢ ( ( 𝑅 ∈ Grp ∧ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V ) → ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∈ Grp )
8 3 5 7 sylancl ⊢ ( 𝜑 → ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∈ Grp )
9 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
10 6 9 pwsbas ⊢ ( ( 𝑅 ∈ Grp ∧ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V ) → ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) = ( Base ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) )
11 3 5 10 sylancl ⊢ ( 𝜑 → ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) = ( Base ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) )
12 eqid ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
13 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
14 1 9 12 13 2 psrbas ⊢ ( 𝜑 → ( Base ‘ 𝑆 ) = ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
15 14 eqcomd ⊢ ( 𝜑 → ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) = ( Base ‘ 𝑆 ) )
16 eqid ⊢ ( Base ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) = ( Base ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
17 3 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) ) → 𝑅 ∈ Grp )
18 5 a1i ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) ) → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V )
19 11 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ↔ 𝑥 ∈ ( Base ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) ) )
20 19 biimpa ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) → 𝑥 ∈ ( Base ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) )
21 20 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) ) → 𝑥 ∈ ( Base ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) )
22 11 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ↔ 𝑦 ∈ ( Base ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) ) )
23 22 biimpa ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) → 𝑦 ∈ ( Base ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) )
24 23 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) ) → 𝑦 ∈ ( Base ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) )
25 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
26 eqid ⊢ ( +g ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) = ( +g ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
27 6 16 17 18 21 24 25 26 pwsplusgval ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) ) → ( 𝑥 ( +g ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) 𝑦 ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) )
28 eqid ⊢ ( +g ‘ 𝑆 ) = ( +g ‘ 𝑆 )
29 14 eleq2d ⊢ ( 𝜑 → ( 𝑥 ∈ ( Base ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) )
30 29 biimpar ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
31 30 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) ) → 𝑥 ∈ ( Base ‘ 𝑆 ) )
32 14 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ ( Base ‘ 𝑆 ) ↔ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) )
33 32 biimpar ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
34 33 adantrl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) ) → 𝑦 ∈ ( Base ‘ 𝑆 ) )
35 1 13 25 28 31 34 psradd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) ) → ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) = ( 𝑥 ∘f ( +g ‘ 𝑅 ) 𝑦 ) )
36 27 35 eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∧ 𝑦 ∈ ( ( Base ‘ 𝑅 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) ) → ( 𝑥 ( +g ‘ ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ) 𝑦 ) = ( 𝑥 ( +g ‘ 𝑆 ) 𝑦 ) )
37 11 15 36 grppropd ⊢ ( 𝜑 → ( ( 𝑅 ↑s { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ∈ Grp ↔ 𝑆 ∈ Grp ) )
38 8 37 mpbid ⊢ ( 𝜑 → 𝑆 ∈ Grp )