Metamath Proof Explorer

Theorem mat1mhm

Description: There is a monoid homomorphism from the multiplicative group of a ring to the multiplicative 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 ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } )
mat1mhm.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
mat1mhm.n ⊢ 𝑁 = ( mulGrp ‘ 𝐴 )
Assertion mat1mhm ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) )

Proof

Step Hyp Ref Expression
1 mat1rhmval.k ⊢ 𝐾 = ( Base ‘ 𝑅 )
2 mat1rhmval.a ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 )
3 mat1rhmval.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
4 mat1rhmval.o ⊢ 𝑂 = ⟨ 𝐸 , 𝐸 ⟩
5 mat1rhmval.f ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } )
6 mat1mhm.m ⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
7 mat1mhm.n ⊢ 𝑁 = ( mulGrp ‘ 𝐴 )
8 6 ringmgp ⊢ ( 𝑅 ∈ Ring → 𝑀 ∈ Mnd )
9 8 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑀 ∈ Mnd )
10 snfi ⊢ { 𝐸 } ∈ Fin
11 simpl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ∈ Ring )
12 2 matring ⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
13 10 11 12 sylancr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐴 ∈ Ring )
14 7 ringmgp ⊢ ( 𝐴 ∈ Ring → 𝑁 ∈ Mnd )
15 13 14 syl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑁 ∈ Mnd )
16 1 2 3 4 5 mat1f ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 : 𝐾 ⟶ 𝐵 )
17 ringmnd ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
18 17 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ∈ Mnd )
19 18 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑅 ∈ Mnd )
20 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐸 ∈ 𝑉 )
21 20 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝐸 ∈ 𝑉 )
22 simpll ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑅 ∈ Ring )
23 eqid ⊢ ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
24 snidg ⊢ ( 𝐸 ∈ 𝑉 → 𝐸 ∈ { 𝐸 } )
25 24 ad2antlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝐸 ∈ { 𝐸 } )
26 simprl ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑤 ∈ 𝐾 )
27 1 2 23 4 5 mat1rhmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑤 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑤 ) ∈ ( Base ‘ 𝐴 ) )
28 22 21 26 27 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ ( Base ‘ 𝐴 ) )
29 2 1 23 25 25 28 matecld ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) ∈ 𝐾 )
30 simprr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝑦 ∈ 𝐾 )
31 1 2 23 4 5 mat1rhmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝐴 ) )
32 22 21 30 31 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ ( Base ‘ 𝐴 ) )
33 2 1 23 25 25 32 matecld ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ∈ 𝐾 )
34 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
35 1 34 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) ∈ 𝐾 ∧ ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ∈ 𝐾 ) → ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) ∈ 𝐾 )
36 22 29 33 35 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) ∈ 𝐾 )
37 oveq2 ⊢ ( 𝑒 = 𝐸 → ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝑒 ) = ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) )
38 oveq1 ⊢ ( 𝑒 = 𝐸 → ( 𝑒 ( 𝐹 ‘ 𝑦 ) 𝐸 ) = ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) )
39 37 38 oveq12d ⊢ ( 𝑒 = 𝐸 → ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑒 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) = ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) )
40 39 adantl ⊢ ( ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) ∧ 𝑒 = 𝐸 ) → ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑒 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) = ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) )
41 1 19 21 36 40 gsumsnd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑅 Σg ( 𝑒 ∈ { 𝐸 } ↦ ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑒 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) ) ) = ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) )
42 1 2 3 4 5 mat1rhmelval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑤 ∈ 𝐾 ) → ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) = 𝑤 )
43 22 21 26 42 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) = 𝑤 )
44 1 2 3 4 5 mat1rhmelval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) = 𝑦 )
45 22 21 30 44 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) = 𝑦 )
46 43 45 oveq12d ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝐸 ) ( .r ‘ 𝑅 ) ( 𝐸 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) = ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) )
47 41 46 eqtrd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑅 Σg ( 𝑒 ∈ { 𝐸 } ↦ ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑒 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) ) ) = ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) )
48 1 2 3 4 5 mat1rhmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑤 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 )
49 22 21 26 48 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 )
50 1 2 3 4 5 mat1rhmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑦 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
51 22 21 30 50 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 )
52 49 51 jca ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ) )
53 24 24 jca ⊢ ( 𝐸 ∈ 𝑉 → ( 𝐸 ∈ { 𝐸 } ∧ 𝐸 ∈ { 𝐸 } ) )
54 53 ad2antlr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ∈ { 𝐸 } ∧ 𝐸 ∈ { 𝐸 } ) )
55 eqid ⊢ ( .r ‘ 𝐴 ) = ( .r ‘ 𝐴 )
56 2 3 55 matmulcell ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ) ∧ ( 𝐸 ∈ { 𝐸 } ∧ 𝐸 ∈ { 𝐸 } ) ) → ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) = ( 𝑅 Σg ( 𝑒 ∈ { 𝐸 } ↦ ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑒 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) ) ) )
57 22 52 54 56 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) = ( 𝑅 Σg ( 𝑒 ∈ { 𝐸 } ↦ ( ( 𝐸 ( 𝐹 ‘ 𝑤 ) 𝑒 ) ( .r ‘ 𝑅 ) ( 𝑒 ( 𝐹 ‘ 𝑦 ) 𝐸 ) ) ) ) )
58 1 34 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) → ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐾 )
59 22 26 30 58 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐾 )
60 1 2 3 4 5 mat1rhmelval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐾 ) → ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) )
61 22 21 59 60 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) )
62 47 57 61 3eqtr4rd ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) )
63 oveq1 ⊢ ( 𝑖 = 𝐸 → ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) )
64 oveq1 ⊢ ( 𝑖 = 𝐸 → ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) )
65 63 64 eqeq12d ⊢ ( 𝑖 = 𝐸 → ( ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ↔ ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ) )
66 oveq2 ⊢ ( 𝑗 = 𝐸 → ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) )
67 oveq2 ⊢ ( 𝑗 = 𝐸 → ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) )
68 66 67 eqeq12d ⊢ ( 𝑗 = 𝐸 → ( ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ↔ ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) ) )
69 65 68 2ralsng ⊢ ( ( 𝐸 ∈ 𝑉 ∧ 𝐸 ∈ 𝑉 ) → ( ∀ 𝑖 ∈ { 𝐸 } ∀ 𝑗 ∈ { 𝐸 } ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ↔ ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) ) )
70 20 69 sylancom ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( ∀ 𝑖 ∈ { 𝐸 } ∀ 𝑗 ∈ { 𝐸 } ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ↔ ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) ) )
71 70 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ∀ 𝑖 ∈ { 𝐸 } ∀ 𝑗 ∈ { 𝐸 } ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ↔ ( 𝐸 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝐸 ) = ( 𝐸 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝐸 ) ) )
72 62 71 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ∀ 𝑖 ∈ { 𝐸 } ∀ 𝑗 ∈ { 𝐸 } ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) )
73 1 2 3 4 5 mat1rhmcl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ∈ 𝐾 ) → ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) ∈ 𝐵 )
74 22 21 59 73 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) ∈ 𝐵 )
75 13 adantr ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → 𝐴 ∈ Ring )
76 3 55 ringcl ⊢ ( ( 𝐴 ∈ Ring ∧ ( 𝐹 ‘ 𝑤 ) ∈ 𝐵 ∧ ( 𝐹 ‘ 𝑦 ) ∈ 𝐵 ) → ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 )
77 75 49 51 76 syl3anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 )
78 2 3 eqmat ⊢ ( ( ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) ∈ 𝐵 ∧ ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) ∈ 𝐵 ) → ( ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑖 ∈ { 𝐸 } ∀ 𝑗 ∈ { 𝐸 } ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ) )
79 74 77 78 syl2anc ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) ↔ ∀ 𝑖 ∈ { 𝐸 } ∀ 𝑗 ∈ { 𝐸 } ( 𝑖 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) 𝑗 ) = ( 𝑖 ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) 𝑗 ) ) )
80 72 79 mpbird ⊢ ( ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) ∧ ( 𝑤 ∈ 𝐾 ∧ 𝑦 ∈ 𝐾 ) ) → ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) )
81 80 ralrimivva ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ∀ 𝑤 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) )
82 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
83 1 82 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐾 )
84 83 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 1r ‘ 𝑅 ) ∈ 𝐾 )
85 1 2 3 4 5 mat1rhmval ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ ( 1r ‘ 𝑅 ) ∈ 𝐾 ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = { ⟨ 𝑂 , ( 1r ‘ 𝑅 ) ⟩ } )
86 84 85 mpd3an3 ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = { ⟨ 𝑂 , ( 1r ‘ 𝑅 ) ⟩ } )
87 2 1 4 mat1dimid ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 1r ‘ 𝐴 ) = { ⟨ 𝑂 , ( 1r ‘ 𝑅 ) ⟩ } )
88 86 87 eqtr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝐴 ) )
89 16 81 88 3jca ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝐹 : 𝐾 ⟶ 𝐵 ∧ ∀ 𝑤 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝐴 ) ) )
90 6 1 mgpbas ⊢ 𝐾 = ( Base ‘ 𝑀 )
91 7 3 mgpbas ⊢ 𝐵 = ( Base ‘ 𝑁 )
92 6 34 mgpplusg ⊢ ( .r ‘ 𝑅 ) = ( +g ‘ 𝑀 )
93 7 55 mgpplusg ⊢ ( .r ‘ 𝐴 ) = ( +g ‘ 𝑁 )
94 6 82 ringidval ⊢ ( 1r ‘ 𝑅 ) = ( 0g ‘ 𝑀 )
95 eqid ⊢ ( 1r ‘ 𝐴 ) = ( 1r ‘ 𝐴 )
96 7 95 ringidval ⊢ ( 1r ‘ 𝐴 ) = ( 0g ‘ 𝑁 )
97 90 91 92 93 94 96 ismhm ⊢ ( 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) ↔ ( ( 𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd ) ∧ ( 𝐹 : 𝐾 ⟶ 𝐵 ∧ ∀ 𝑤 ∈ 𝐾 ∀ 𝑦 ∈ 𝐾 ( 𝐹 ‘ ( 𝑤 ( .r ‘ 𝑅 ) 𝑦 ) ) = ( ( 𝐹 ‘ 𝑤 ) ( .r ‘ 𝐴 ) ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ ( 1r ‘ 𝑅 ) ) = ( 1r ‘ 𝐴 ) ) ) )
98 9 15 89 97 syl21anbrc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑀 MndHom 𝑁 ) )