This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem rhmpsr

Description: Provide a ring homomorphism between two power series algebras over their respective base rings given a ring homomorphism between the two base rings. (Contributed by SN, 8-Feb-2025)

Ref Expression
Hypotheses rhmpsr.p ⊢ 𝑃 = ( 𝐼 mPwSer 𝑅 )
rhmpsr.q ⊢ 𝑄 = ( 𝐼 mPwSer 𝑆 )
rhmpsr.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
rhmpsr.f ⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
rhmpsr.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
rhmpsr.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
Assertion rhmpsr ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )

Proof

Step Hyp Ref Expression
1 rhmpsr.p ⊢ 𝑃 = ( 𝐼 mPwSer 𝑅 )
2 rhmpsr.q ⊢ 𝑄 = ( 𝐼 mPwSer 𝑆 )
3 rhmpsr.b ⊢ 𝐵 = ( Base ‘ 𝑃 )
4 rhmpsr.f ⊢ 𝐹 = ( 𝑝 ∈ 𝐵 ↦ ( 𝐻 ∘ 𝑝 ) )
5 rhmpsr.i ⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
6 rhmpsr.h ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
7 eqid ⊢ ( 1r ‘ 𝑃 ) = ( 1r ‘ 𝑃 )
8 eqid ⊢ ( 1r ‘ 𝑄 ) = ( 1r ‘ 𝑄 )
9 eqid ⊢ ( .r ‘ 𝑃 ) = ( .r ‘ 𝑃 )
10 eqid ⊢ ( .r ‘ 𝑄 ) = ( .r ‘ 𝑄 )
11 rhmrcl1 ⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑅 ∈ Ring )
12 6 11 syl ⊢ ( 𝜑 → 𝑅 ∈ Ring )
13 1 5 12 psrring ⊢ ( 𝜑 → 𝑃 ∈ Ring )
14 rhmrcl2 ⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝑆 ∈ Ring )
15 6 14 syl ⊢ ( 𝜑 → 𝑆 ∈ Ring )
16 2 5 15 psrring ⊢ ( 𝜑 → 𝑄 ∈ Ring )
17 eqid ⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
18 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
19 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
20 1 5 12 17 18 19 7 psr1 ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) )
21 20 coeq2d ⊢ ( 𝜑 → ( 𝐻 ∘ ( 1r ‘ 𝑃 ) ) = ( 𝐻 ∘ ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
22 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
23 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
24 22 23 rhmf ⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
25 6 24 syl ⊢ ( 𝜑 → 𝐻 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
26 22 19 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
27 12 26 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
28 22 18 ring0cl ⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
29 12 28 syl ⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
30 27 29 ifcld ⊢ ( 𝜑 → if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
31 30 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) → if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑅 ) )
32 25 31 cofmpt ⊢ ( 𝜑 → ( 𝐻 ∘ ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) )
33 fvif ⊢ ( 𝐻 ‘ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 𝐻 ‘ ( 1r ‘ 𝑅 ) ) , ( 𝐻 ‘ ( 0g ‘ 𝑅 ) ) )
34 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
35 19 34 rhm1 ⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐻 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
36 6 35 syl ⊢ ( 𝜑 → ( 𝐻 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝑆 ) )
37 rhmghm ⊢ ( 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) )
38 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
39 18 38 ghmid ⊢ ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐻 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
40 6 37 39 3syl ⊢ ( 𝜑 → ( 𝐻 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
41 36 40 ifeq12d ⊢ ( 𝜑 → if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 𝐻 ‘ ( 1r ‘ 𝑅 ) ) , ( 𝐻 ‘ ( 0g ‘ 𝑅 ) ) ) = if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑆 ) , ( 0g ‘ 𝑆 ) ) )
42 33 41 eqtrid ⊢ ( 𝜑 → ( 𝐻 ‘ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) = if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑆 ) , ( 0g ‘ 𝑆 ) ) )
43 42 mpteq2dv ⊢ ( 𝜑 → ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ ( 𝐻 ‘ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑅 ) , ( 0g ‘ 𝑅 ) ) ) ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑆 ) , ( 0g ‘ 𝑆 ) ) ) )
44 21 32 43 3eqtrd ⊢ ( 𝜑 → ( 𝐻 ∘ ( 1r ‘ 𝑃 ) ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑆 ) , ( 0g ‘ 𝑆 ) ) ) )
45 coeq2 ⊢ ( 𝑝 = ( 1r ‘ 𝑃 ) → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ ( 1r ‘ 𝑃 ) ) )
46 3 7 ringidcl ⊢ ( 𝑃 ∈ Ring → ( 1r ‘ 𝑃 ) ∈ 𝐵 )
47 13 46 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑃 ) ∈ 𝐵 )
48 6 47 coexd ⊢ ( 𝜑 → ( 𝐻 ∘ ( 1r ‘ 𝑃 ) ) ∈ V )
49 4 45 47 48 fvmptd3 ⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑃 ) ) = ( 𝐻 ∘ ( 1r ‘ 𝑃 ) ) )
50 2 5 15 17 38 34 8 psr1 ⊢ ( 𝜑 → ( 1r ‘ 𝑄 ) = ( 𝑑 ∈ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ↦ if ( 𝑑 = ( 𝐼 × { 0 } ) , ( 1r ‘ 𝑆 ) , ( 0g ‘ 𝑆 ) ) ) )
51 44 49 50 3eqtr4d ⊢ ( 𝜑 → ( 𝐹 ‘ ( 1r ‘ 𝑃 ) ) = ( 1r ‘ 𝑄 ) )
52 eqid ⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
53 6 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐻 ∈ ( 𝑅 RingHom 𝑆 ) )
54 simprl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑥 ∈ 𝐵 )
55 simprr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑦 ∈ 𝐵 )
56 1 2 3 52 9 10 53 54 55 rhmcomulpsr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
57 coeq2 ⊢ ( 𝑝 = ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) )
58 13 adantr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ Ring )
59 3 9 58 54 55 ringcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 )
60 53 59 coexd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) ∈ V )
61 4 57 59 60 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( 𝐻 ∘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) )
62 coeq2 ⊢ ( 𝑝 = 𝑥 → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ 𝑥 ) )
63 53 54 coexd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ 𝑥 ) ∈ V )
64 4 62 54 63 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐻 ∘ 𝑥 ) )
65 coeq2 ⊢ ( 𝑝 = 𝑦 → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ 𝑦 ) )
66 53 55 coexd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ 𝑦 ) ∈ V )
67 4 65 55 66 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ 𝑦 ) = ( 𝐻 ∘ 𝑦 ) )
68 64 67 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
69 56 61 68 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( .r ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( .r ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) )
70 eqid ⊢ ( +g ‘ 𝑃 ) = ( +g ‘ 𝑃 )
71 eqid ⊢ ( +g ‘ 𝑄 ) = ( +g ‘ 𝑄 )
72 ghmmhm ⊢ ( 𝐻 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
73 6 37 72 3syl ⊢ ( 𝜑 → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
74 73 adantr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
75 simpr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → 𝑝 ∈ 𝐵 )
76 1 2 3 52 74 75 mhmcopsr ⊢ ( ( 𝜑 ∧ 𝑝 ∈ 𝐵 ) → ( 𝐻 ∘ 𝑝 ) ∈ ( Base ‘ 𝑄 ) )
77 76 4 fmptd ⊢ ( 𝜑 → 𝐹 : 𝐵 ⟶ ( Base ‘ 𝑄 ) )
78 53 37 72 3syl ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝐻 ∈ ( 𝑅 MndHom 𝑆 ) )
79 1 2 3 52 70 71 78 54 55 mhmcoaddpsr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
80 coeq2 ⊢ ( 𝑝 = ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) → ( 𝐻 ∘ 𝑝 ) = ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) )
81 58 ringgrpd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → 𝑃 ∈ Grp )
82 3 70 81 54 55 grpcld ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ∈ 𝐵 )
83 53 82 coexd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) ∈ V )
84 4 80 82 83 fvmptd3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( 𝐻 ∘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) )
85 64 67 oveq12d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) = ( ( 𝐻 ∘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐻 ∘ 𝑦 ) ) )
86 79 84 85 3eqtr4d ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝐹 ‘ ( 𝑥 ( +g ‘ 𝑃 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ( +g ‘ 𝑄 ) ( 𝐹 ‘ 𝑦 ) ) )
87 3 7 8 9 10 13 16 51 69 52 70 71 77 86 isrhmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝑃 RingHom 𝑄 ) )