Metamath Proof Explorer

Theorem mat1ghm

Description: There is a group homomorphism from the additive group of a ring to the additive group of the ring of matrices with dimension 1 over this ring. (Contributed by AV, 22-Dec-2019)

Ref Expression
Hypotheses mat1rhmval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
mat1rhmval.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
mat1rhmval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
mat1rhmval.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
mat1rhmval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } )
Assertion mat1ghm ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝐴 ) )

Proof

Step Hyp Ref Expression
1 mat1rhmval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 mat1rhmval.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
3 mat1rhmval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 mat1rhmval.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
5 mat1rhmval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } )
6 eqid ⊢ ( +g ‘ 𝑅 ) = ( +g ‘ 𝑅 )
7 eqid ⊢ ( +g ‘ 𝐴 ) = ( +g ‘ 𝐴 )
8 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
9 8 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ∈ Grp )
10 snfi ⊢ { 𝐸 } ∈ Fin
11 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ∈ Ring )
12 2 matgrp ⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Grp )
13 10 11 12 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐴 ∈ Grp )
14 1 2 3 4 5 mat1f ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 : 𝐾 ⟶ 𝐵 )
15 11 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑅 ∈ Ring )
16 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐸 ∈ 𝑉 )
17 16 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝐸 ∈ 𝑉 )
18 simpl ⊢ ( ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → 𝑤 ∈ 𝐾 )
19 18 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑤 ∈ 𝐾 )
20 1 2 3 4 5 mat1rhmelval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑤 ∈ 𝐾 ) → ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) = 𝑤 )
21 15 17 19 20 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) = 𝑤 )
22 simpr ⊢ ( ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → 𝑦 ∈ 𝐾 )
23 22 adantl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑦 ∈ 𝐾 )
24 1 2 3 4 5 mat1rhmelval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) = 𝑦 )
25 15 17 23 24 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) = 𝑦 )
26 21 25 oveq12d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) ( +g ‘ 𝑅 ) ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) = ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) )
27 1 2 3 4 5 mat1rhmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑤 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 )
28 15 17 19 27 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 )
29 1 2 3 4 5 mat1rhmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
30 15 17 23 29 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
31 snidg ⊢ ( 𝐸 ∈ 𝑉 → 𝐸 ∈ { 𝐸 } )
32 31 31 jca ⊢ ( 𝐸 ∈ 𝑉 → ( 𝐸 ∈ { 𝐸 } ∧ 𝐸 ∈ { 𝐸 } ) )
33 32 adantl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝐸 ∈ { 𝐸 } ∧ 𝐸 ∈ { 𝐸 } ) )
34 33 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ∈ { 𝐸 } ∧ 𝐸 ∈ { 𝐸 } ) )
35 2 3 7 6 matplusgcell ⊢ ( ( ( ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ) ∧ ( 𝐸 ∈ { 𝐸 } ∧ 𝐸 ∈ { 𝐸 } ) ) → ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) = ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) ( +g ‘ 𝑅 ) ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) )
36 28 30 34 35 syl21anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) = ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) ( +g ‘ 𝑅 ) ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) )
37 1 6 ringacl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐾 )
38 15 19 23 37 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐾 )
39 1 2 3 4 5 mat1rhmelval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐾 ) → ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) )
40 15 17 38 39 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) )
41 26 36 40 3eqtr4rd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) )
42 oveq1 ⊢ ( 𝑖 = 𝐸 → ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) )
43 oveq1 ⊢ ( 𝑖 = 𝐸 → ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) )
44 42 43 eqeq12d ⊢ ( 𝑖 = 𝐸 → ( ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ↔ ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ) )
45 oveq2 ⊢ ( 𝑗 = 𝐸 → ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) )
46 oveq2 ⊢ ( 𝑗 = 𝐸 → ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) )
47 45 46 eqeq12d ⊢ ( 𝑗 = 𝐸 → ( ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ↔ ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) ) )
48 44 47 2ralsng ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ) → ( ∀ 𝑖 ∈ { 𝐸 } ∀ 𝑗 ∈ { 𝐸 } ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ↔ ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) ) )
49 16 16 48 syl2anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( ∀ 𝑖 ∈ { 𝐸 } ∀ 𝑗 ∈ { 𝐸 } ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ↔ ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) ) )
50 49 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ∀ 𝑖 ∈ { 𝐸 } ∀ 𝑗 ∈ { 𝐸 } ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ↔ ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) ) )
51 41 50 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ∀ 𝑖 ∈ { 𝐸 } ∀ 𝑗 ∈ { 𝐸 } ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) )
52 1 2 3 4 5 mat1rhmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ∈ 𝐾 ) → ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) ∈ 𝐵 )
53 15 17 38 52 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) ∈ 𝐵 )
54 2 matring ⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
55 10 11 54 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐴 ∈ Ring )
56 55 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝐴 ∈ Ring )
57 3 7 ringacl ⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 )
58 56 28 30 57 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 )
59 2 3 eqmat ⊢ ( ( ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 ) → ( ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑖 ∈ { 𝐸 } ∀ 𝑗 ∈ { 𝐸 } ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ) )
60 53 58 59 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑖 ∈ { 𝐸 } ∀ 𝑗 ∈ { 𝐸 } ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ) )
61 51 60 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑤 ( +g ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑤 ) ( +g ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) )
62 1 3 6 7 9 13 14 61 isghmd ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝐴 ) )