Metamath Proof Explorer

Theorem pwsdiagrhm

Description: Diagonal homomorphism into a structure power (Rings). (Contributed by Mario Carneiro, 12-Mar-2015) (Revised by Mario Carneiro, 6-May-2015)

Ref Expression
Hypotheses pwsdiagrhm.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
pwsdiagrhm.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
pwsdiagrhm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐼 × { 𝑥 } ) )
Assertion pwsdiagrhm ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑌 ) )

Proof

Step Hyp Ref Expression
1 pwsdiagrhm.y ⊢ 𝑌 = ( 𝑅 ↑s 𝐼 )
2 pwsdiagrhm.b ⊢ 𝐵 = ( Base ‘ 𝑅 )
3 pwsdiagrhm.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐵 ↦ ( 𝐼 × { 𝑥 } ) )
4 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑅 ∈ Ring )
5 1 pwsring ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝑌 ∈ Ring )
6 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
7 1 2 3 pwsdiagghm ⊢ ( ( 𝑅 ∈ Grp ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑌 ) )
8 6 7 sylan ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑌 ) )
9 eqid ⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
10 9 ringmgp ⊢ ( 𝑅 ∈ Ring → ( mulGrp ‘ 𝑅 ) ∈ Mnd )
11 eqid ⊢ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) = ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 )
12 9 2 mgpbas ⊢ 𝐵 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
13 11 12 3 pwsdiagmhm ⊢ ( ( ( mulGrp ‘ 𝑅 ) ∈ Mnd ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) ) )
14 10 13 sylan ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) ) )
15 eqidd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ ( mulGrp ‘ 𝑅 ) ) = ( Base ‘ ( mulGrp ‘ 𝑅 ) ) )
16 eqidd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( mulGrp ‘ 𝑌 ) ) )
17 eqid ⊢ ( mulGrp ‘ 𝑌 ) = ( mulGrp ‘ 𝑌 )
18 eqid ⊢ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( mulGrp ‘ 𝑌 ) )
19 eqid ⊢ ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) )
20 eqid ⊢ ( +g ‘ ( mulGrp ‘ 𝑌 ) ) = ( +g ‘ ( mulGrp ‘ 𝑌 ) )
21 eqid ⊢ ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) )
22 1 9 11 17 18 19 20 21 pwsmgp ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) ) ∧ ( +g ‘ ( mulGrp ‘ 𝑌 ) ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) ) ) )
23 22 simpld ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( Base ‘ ( mulGrp ‘ 𝑌 ) ) = ( Base ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) ) )
24 eqidd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑦 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ∧ 𝑧 ∈ ( Base ‘ ( mulGrp ‘ 𝑅 ) ) ) ) → ( 𝑦 ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) = ( 𝑦 ( +g ‘ ( mulGrp ‘ 𝑅 ) ) 𝑧 ) )
25 22 simprd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( +g ‘ ( mulGrp ‘ 𝑌 ) ) = ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) ) )
26 25 oveqdr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) ∧ ( 𝑦 ∈ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) ∧ 𝑧 ∈ ( Base ‘ ( mulGrp ‘ 𝑌 ) ) ) ) → ( 𝑦 ( +g ‘ ( mulGrp ‘ 𝑌 ) ) 𝑧 ) = ( 𝑦 ( +g ‘ ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) ) 𝑧 ) )
27 15 16 15 23 24 26 mhmpropd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑌 ) ) = ( ( mulGrp ‘ 𝑅 ) MndHom ( ( mulGrp ‘ 𝑅 ) ↑s 𝐼 ) ) )
28 14 27 eleqtrrd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑌 ) ) )
29 8 28 jca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → ( 𝐹 ∈ ( 𝑅 GrpHom 𝑌 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑌 ) ) ) )
30 9 17 isrhm ⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑌 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝑌 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑌 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑌 ) ) ) ) )
31 4 5 29 30 syl21anbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐼 ∈ 𝑊 ) → 𝐹 ∈ ( 𝑅 RingHom 𝑌 ) )