Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  mat1mhm Structured version   Visualization version   GIF version

Theorem mat1mhm 21185
 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.)
Hypotheses
Ref Expression
mat1rhmval.k 𝐾 = (Base‘𝑅)
mat1rhmval.a 𝐴 = ({𝐸} Mat 𝑅)
mat1rhmval.b 𝐵 = (Base‘𝐴)
mat1rhmval.o 𝑂 = ⟨𝐸, 𝐸
mat1rhmval.f 𝐹 = (𝑥𝐾 ↦ {⟨𝑂, 𝑥⟩})
mat1mhm.m 𝑀 = (mulGrp‘𝑅)
mat1mhm.n 𝑁 = (mulGrp‘𝐴)
Assertion
Ref Expression
mat1mhm ((𝑅 ∈ Ring ∧ 𝐸𝑉) → 𝐹 ∈ (𝑀 MndHom 𝑁))
Distinct variable groups:   𝑥,𝐾   𝑥,𝑂   𝑥,𝐸   𝑥,𝑅   𝑥,𝑉   𝑥,𝐵   𝑥,𝐴   𝑥,𝐹   𝑥,𝑀   𝑥,𝑁

Proof of Theorem mat1mhm
Dummy variables 𝑖 𝑗 𝑤 𝑦 𝑒 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mat1mhm.m . . . 4 𝑀 = (mulGrp‘𝑅)
21ringmgp 19372 . . 3 (𝑅 ∈ Ring → 𝑀 ∈ Mnd)
32adantr 485 . 2 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → 𝑀 ∈ Mnd)
4 snfi 8615 . . . 4 {𝐸} ∈ Fin
5 simpl 487 . . . 4 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → 𝑅 ∈ Ring)
6 mat1rhmval.a . . . . 5 𝐴 = ({𝐸} Mat 𝑅)
76matring 21144 . . . 4 (({𝐸} ∈ Fin ∧ 𝑅 ∈ Ring) → 𝐴 ∈ Ring)
84, 5, 7sylancr 591 . . 3 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → 𝐴 ∈ Ring)
9 mat1mhm.n . . . 4 𝑁 = (mulGrp‘𝐴)
109ringmgp 19372 . . 3 (𝐴 ∈ Ring → 𝑁 ∈ Mnd)
118, 10syl 17 . 2 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → 𝑁 ∈ Mnd)
12 mat1rhmval.k . . . 4 𝐾 = (Base‘𝑅)
13 mat1rhmval.b . . . 4 𝐵 = (Base‘𝐴)
14 mat1rhmval.o . . . 4 𝑂 = ⟨𝐸, 𝐸
15 mat1rhmval.f . . . 4 𝐹 = (𝑥𝐾 ↦ {⟨𝑂, 𝑥⟩})
1612, 6, 13, 14, 15mat1f 21183 . . 3 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → 𝐹:𝐾𝐵)
17 ringmnd 19376 . . . . . . . . . . 11 (𝑅 ∈ Ring → 𝑅 ∈ Mnd)
1817adantr 485 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → 𝑅 ∈ Mnd)
1918adantr 485 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → 𝑅 ∈ Mnd)
20 simpr 489 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → 𝐸𝑉)
2120adantr 485 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → 𝐸𝑉)
22 simpll 767 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → 𝑅 ∈ Ring)
23 eqid 2759 . . . . . . . . . . 11 (Base‘𝐴) = (Base‘𝐴)
24 snidg 4557 . . . . . . . . . . . 12 (𝐸𝑉𝐸 ∈ {𝐸})
2524ad2antlr 727 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → 𝐸 ∈ {𝐸})
26 simprl 771 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → 𝑤𝐾)
2712, 6, 23, 14, 15mat1rhmcl 21182 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ 𝐸𝑉𝑤𝐾) → (𝐹𝑤) ∈ (Base‘𝐴))
2822, 21, 26, 27syl3anc 1369 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐹𝑤) ∈ (Base‘𝐴))
296, 12, 23, 25, 25, 28matecld 21127 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐸(𝐹𝑤)𝐸) ∈ 𝐾)
30 simprr 773 . . . . . . . . . . . 12 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → 𝑦𝐾)
3112, 6, 23, 14, 15mat1rhmcl 21182 . . . . . . . . . . . 12 ((𝑅 ∈ Ring ∧ 𝐸𝑉𝑦𝐾) → (𝐹𝑦) ∈ (Base‘𝐴))
3222, 21, 30, 31syl3anc 1369 . . . . . . . . . . 11 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐹𝑦) ∈ (Base‘𝐴))
336, 12, 23, 25, 25, 32matecld 21127 . . . . . . . . . 10 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐸(𝐹𝑦)𝐸) ∈ 𝐾)
34 eqid 2759 . . . . . . . . . . 11 (.r𝑅) = (.r𝑅)
3512, 34ringcl 19383 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ (𝐸(𝐹𝑤)𝐸) ∈ 𝐾 ∧ (𝐸(𝐹𝑦)𝐸) ∈ 𝐾) → ((𝐸(𝐹𝑤)𝐸)(.r𝑅)(𝐸(𝐹𝑦)𝐸)) ∈ 𝐾)
3622, 29, 33, 35syl3anc 1369 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → ((𝐸(𝐹𝑤)𝐸)(.r𝑅)(𝐸(𝐹𝑦)𝐸)) ∈ 𝐾)
37 oveq2 7159 . . . . . . . . . . 11 (𝑒 = 𝐸 → (𝐸(𝐹𝑤)𝑒) = (𝐸(𝐹𝑤)𝐸))
38 oveq1 7158 . . . . . . . . . . 11 (𝑒 = 𝐸 → (𝑒(𝐹𝑦)𝐸) = (𝐸(𝐹𝑦)𝐸))
3937, 38oveq12d 7169 . . . . . . . . . 10 (𝑒 = 𝐸 → ((𝐸(𝐹𝑤)𝑒)(.r𝑅)(𝑒(𝐹𝑦)𝐸)) = ((𝐸(𝐹𝑤)𝐸)(.r𝑅)(𝐸(𝐹𝑦)𝐸)))
4039adantl 486 . . . . . . . . 9 ((((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) ∧ 𝑒 = 𝐸) → ((𝐸(𝐹𝑤)𝑒)(.r𝑅)(𝑒(𝐹𝑦)𝐸)) = ((𝐸(𝐹𝑤)𝐸)(.r𝑅)(𝐸(𝐹𝑦)𝐸)))
4112, 19, 21, 36, 40gsumsnd 19141 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝑅 Σg (𝑒 ∈ {𝐸} ↦ ((𝐸(𝐹𝑤)𝑒)(.r𝑅)(𝑒(𝐹𝑦)𝐸)))) = ((𝐸(𝐹𝑤)𝐸)(.r𝑅)(𝐸(𝐹𝑦)𝐸)))
4212, 6, 13, 14, 15mat1rhmelval 21181 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝐸𝑉𝑤𝐾) → (𝐸(𝐹𝑤)𝐸) = 𝑤)
4322, 21, 26, 42syl3anc 1369 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐸(𝐹𝑤)𝐸) = 𝑤)
4412, 6, 13, 14, 15mat1rhmelval 21181 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝐸𝑉𝑦𝐾) → (𝐸(𝐹𝑦)𝐸) = 𝑦)
4522, 21, 30, 44syl3anc 1369 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐸(𝐹𝑦)𝐸) = 𝑦)
4643, 45oveq12d 7169 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → ((𝐸(𝐹𝑤)𝐸)(.r𝑅)(𝐸(𝐹𝑦)𝐸)) = (𝑤(.r𝑅)𝑦))
4741, 46eqtrd 2794 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝑅 Σg (𝑒 ∈ {𝐸} ↦ ((𝐸(𝐹𝑤)𝑒)(.r𝑅)(𝑒(𝐹𝑦)𝐸)))) = (𝑤(.r𝑅)𝑦))
4812, 6, 13, 14, 15mat1rhmcl 21182 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝐸𝑉𝑤𝐾) → (𝐹𝑤) ∈ 𝐵)
4922, 21, 26, 48syl3anc 1369 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐹𝑤) ∈ 𝐵)
5012, 6, 13, 14, 15mat1rhmcl 21182 . . . . . . . . . 10 ((𝑅 ∈ Ring ∧ 𝐸𝑉𝑦𝐾) → (𝐹𝑦) ∈ 𝐵)
5122, 21, 30, 50syl3anc 1369 . . . . . . . . 9 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐹𝑦) ∈ 𝐵)
5249, 51jca 516 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → ((𝐹𝑤) ∈ 𝐵 ∧ (𝐹𝑦) ∈ 𝐵))
5324, 24jca 516 . . . . . . . . 9 (𝐸𝑉 → (𝐸 ∈ {𝐸} ∧ 𝐸 ∈ {𝐸}))
5453ad2antlr 727 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐸 ∈ {𝐸} ∧ 𝐸 ∈ {𝐸}))
55 eqid 2759 . . . . . . . . 9 (.r𝐴) = (.r𝐴)
566, 13, 55matmulcell 21146 . . . . . . . 8 ((𝑅 ∈ Ring ∧ ((𝐹𝑤) ∈ 𝐵 ∧ (𝐹𝑦) ∈ 𝐵) ∧ (𝐸 ∈ {𝐸} ∧ 𝐸 ∈ {𝐸})) → (𝐸((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝐸) = (𝑅 Σg (𝑒 ∈ {𝐸} ↦ ((𝐸(𝐹𝑤)𝑒)(.r𝑅)(𝑒(𝐹𝑦)𝐸)))))
5722, 52, 54, 56syl3anc 1369 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐸((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝐸) = (𝑅 Σg (𝑒 ∈ {𝐸} ↦ ((𝐸(𝐹𝑤)𝑒)(.r𝑅)(𝑒(𝐹𝑦)𝐸)))))
5812, 34ringcl 19383 . . . . . . . . 9 ((𝑅 ∈ Ring ∧ 𝑤𝐾𝑦𝐾) → (𝑤(.r𝑅)𝑦) ∈ 𝐾)
5922, 26, 30, 58syl3anc 1369 . . . . . . . 8 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝑤(.r𝑅)𝑦) ∈ 𝐾)
6012, 6, 13, 14, 15mat1rhmelval 21181 . . . . . . . 8 ((𝑅 ∈ Ring ∧ 𝐸𝑉 ∧ (𝑤(.r𝑅)𝑦) ∈ 𝐾) → (𝐸(𝐹‘(𝑤(.r𝑅)𝑦))𝐸) = (𝑤(.r𝑅)𝑦))
6122, 21, 59, 60syl3anc 1369 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐸(𝐹‘(𝑤(.r𝑅)𝑦))𝐸) = (𝑤(.r𝑅)𝑦))
6247, 57, 613eqtr4rd 2805 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐸(𝐹‘(𝑤(.r𝑅)𝑦))𝐸) = (𝐸((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝐸))
63 oveq1 7158 . . . . . . . . . 10 (𝑖 = 𝐸 → (𝑖(𝐹‘(𝑤(.r𝑅)𝑦))𝑗) = (𝐸(𝐹‘(𝑤(.r𝑅)𝑦))𝑗))
64 oveq1 7158 . . . . . . . . . 10 (𝑖 = 𝐸 → (𝑖((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝑗) = (𝐸((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝑗))
6563, 64eqeq12d 2775 . . . . . . . . 9 (𝑖 = 𝐸 → ((𝑖(𝐹‘(𝑤(.r𝑅)𝑦))𝑗) = (𝑖((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(.r𝑅)𝑦))𝑗) = (𝐸((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝑗)))
66 oveq2 7159 . . . . . . . . . 10 (𝑗 = 𝐸 → (𝐸(𝐹‘(𝑤(.r𝑅)𝑦))𝑗) = (𝐸(𝐹‘(𝑤(.r𝑅)𝑦))𝐸))
67 oveq2 7159 . . . . . . . . . 10 (𝑗 = 𝐸 → (𝐸((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝑗) = (𝐸((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝐸))
6866, 67eqeq12d 2775 . . . . . . . . 9 (𝑗 = 𝐸 → ((𝐸(𝐹‘(𝑤(.r𝑅)𝑦))𝑗) = (𝐸((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(.r𝑅)𝑦))𝐸) = (𝐸((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝐸)))
6965, 682ralsng 4574 . . . . . . . 8 ((𝐸𝑉𝐸𝑉) → (∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(.r𝑅)𝑦))𝑗) = (𝑖((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(.r𝑅)𝑦))𝐸) = (𝐸((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝐸)))
7020, 69sylancom 592 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → (∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(.r𝑅)𝑦))𝑗) = (𝑖((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(.r𝑅)𝑦))𝐸) = (𝐸((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝐸)))
7170adantr 485 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(.r𝑅)𝑦))𝑗) = (𝑖((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝑗) ↔ (𝐸(𝐹‘(𝑤(.r𝑅)𝑦))𝐸) = (𝐸((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝐸)))
7262, 71mpbird 260 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → ∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(.r𝑅)𝑦))𝑗) = (𝑖((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝑗))
7312, 6, 13, 14, 15mat1rhmcl 21182 . . . . . . 7 ((𝑅 ∈ Ring ∧ 𝐸𝑉 ∧ (𝑤(.r𝑅)𝑦) ∈ 𝐾) → (𝐹‘(𝑤(.r𝑅)𝑦)) ∈ 𝐵)
7422, 21, 59, 73syl3anc 1369 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐹‘(𝑤(.r𝑅)𝑦)) ∈ 𝐵)
758adantr 485 . . . . . . 7 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → 𝐴 ∈ Ring)
7613, 55ringcl 19383 . . . . . . 7 ((𝐴 ∈ Ring ∧ (𝐹𝑤) ∈ 𝐵 ∧ (𝐹𝑦) ∈ 𝐵) → ((𝐹𝑤)(.r𝐴)(𝐹𝑦)) ∈ 𝐵)
7775, 49, 51, 76syl3anc 1369 . . . . . 6 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → ((𝐹𝑤)(.r𝐴)(𝐹𝑦)) ∈ 𝐵)
786, 13eqmat 21125 . . . . . 6 (((𝐹‘(𝑤(.r𝑅)𝑦)) ∈ 𝐵 ∧ ((𝐹𝑤)(.r𝐴)(𝐹𝑦)) ∈ 𝐵) → ((𝐹‘(𝑤(.r𝑅)𝑦)) = ((𝐹𝑤)(.r𝐴)(𝐹𝑦)) ↔ ∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(.r𝑅)𝑦))𝑗) = (𝑖((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝑗)))
7974, 77, 78syl2anc 588 . . . . 5 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → ((𝐹‘(𝑤(.r𝑅)𝑦)) = ((𝐹𝑤)(.r𝐴)(𝐹𝑦)) ↔ ∀𝑖 ∈ {𝐸}∀𝑗 ∈ {𝐸} (𝑖(𝐹‘(𝑤(.r𝑅)𝑦))𝑗) = (𝑖((𝐹𝑤)(.r𝐴)(𝐹𝑦))𝑗)))
8072, 79mpbird 260 . . . 4 (((𝑅 ∈ Ring ∧ 𝐸𝑉) ∧ (𝑤𝐾𝑦𝐾)) → (𝐹‘(𝑤(.r𝑅)𝑦)) = ((𝐹𝑤)(.r𝐴)(𝐹𝑦)))
8180ralrimivva 3121 . . 3 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → ∀𝑤𝐾𝑦𝐾 (𝐹‘(𝑤(.r𝑅)𝑦)) = ((𝐹𝑤)(.r𝐴)(𝐹𝑦)))
82 eqid 2759 . . . . . . 7 (1r𝑅) = (1r𝑅)
8312, 82ringidcl 19390 . . . . . 6 (𝑅 ∈ Ring → (1r𝑅) ∈ 𝐾)
8483adantr 485 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → (1r𝑅) ∈ 𝐾)
8512, 6, 13, 14, 15mat1rhmval 21180 . . . . 5 ((𝑅 ∈ Ring ∧ 𝐸𝑉 ∧ (1r𝑅) ∈ 𝐾) → (𝐹‘(1r𝑅)) = {⟨𝑂, (1r𝑅)⟩})
8684, 85mpd3an3 1460 . . . 4 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → (𝐹‘(1r𝑅)) = {⟨𝑂, (1r𝑅)⟩})
876, 12, 14mat1dimid 21175 . . . 4 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → (1r𝐴) = {⟨𝑂, (1r𝑅)⟩})
8886, 87eqtr4d 2797 . . 3 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → (𝐹‘(1r𝑅)) = (1r𝐴))
8916, 81, 883jca 1126 . 2 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → (𝐹:𝐾𝐵 ∧ ∀𝑤𝐾𝑦𝐾 (𝐹‘(𝑤(.r𝑅)𝑦)) = ((𝐹𝑤)(.r𝐴)(𝐹𝑦)) ∧ (𝐹‘(1r𝑅)) = (1r𝐴)))
901, 12mgpbas 19314 . . 3 𝐾 = (Base‘𝑀)
919, 13mgpbas 19314 . . 3 𝐵 = (Base‘𝑁)
921, 34mgpplusg 19312 . . 3 (.r𝑅) = (+g𝑀)
939, 55mgpplusg 19312 . . 3 (.r𝐴) = (+g𝑁)
941, 82ringidval 19322 . . 3 (1r𝑅) = (0g𝑀)
95 eqid 2759 . . . 4 (1r𝐴) = (1r𝐴)
969, 95ringidval 19322 . . 3 (1r𝐴) = (0g𝑁)
9790, 91, 92, 93, 94, 96ismhm 18025 . 2 (𝐹 ∈ (𝑀 MndHom 𝑁) ↔ ((𝑀 ∈ Mnd ∧ 𝑁 ∈ Mnd) ∧ (𝐹:𝐾𝐵 ∧ ∀𝑤𝐾𝑦𝐾 (𝐹‘(𝑤(.r𝑅)𝑦)) = ((𝐹𝑤)(.r𝐴)(𝐹𝑦)) ∧ (𝐹‘(1r𝑅)) = (1r𝐴))))
983, 11, 89, 97syl21anbrc 1342 1 ((𝑅 ∈ Ring ∧ 𝐸𝑉) → 𝐹 ∈ (𝑀 MndHom 𝑁))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 400   ∧ w3a 1085   = wceq 1539   ∈ wcel 2112  ∀wral 3071  {csn 4523  ⟨cop 4529   ↦ cmpt 5113  ⟶wf 6332  ‘cfv 6336  (class class class)co 7151  Fincfn 8528  Basecbs 16542  .rcmulr 16625   Σg cgsu 16773  Mndcmnd 17978   MndHom cmhm 18021  mulGrpcmgp 19308  1rcur 19320  Ringcrg 19366   Mat cmat 21108 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2159  ax-12 2176  ax-ext 2730  ax-rep 5157  ax-sep 5170  ax-nul 5177  ax-pow 5235  ax-pr 5299  ax-un 7460  ax-cnex 10632  ax-resscn 10633  ax-1cn 10634  ax-icn 10635  ax-addcl 10636  ax-addrcl 10637  ax-mulcl 10638  ax-mulrcl 10639  ax-mulcom 10640  ax-addass 10641  ax-mulass 10642  ax-distr 10643  ax-i2m1 10644  ax-1ne0 10645  ax-1rid 10646  ax-rnegex 10647  ax-rrecex 10648  ax-cnre 10649  ax-pre-lttri 10650  ax-pre-lttrn 10651  ax-pre-ltadd 10652  ax-pre-mulgt0 10653 This theorem depends on definitions:  df-bi 210  df-an 401  df-or 846  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2071  df-mo 2558  df-eu 2589  df-clab 2737  df-cleq 2751  df-clel 2831  df-nfc 2902  df-ne 2953  df-nel 3057  df-ral 3076  df-rex 3077  df-reu 3078  df-rmo 3079  df-rab 3080  df-v 3412  df-sbc 3698  df-csb 3807  df-dif 3862  df-un 3864  df-in 3866  df-ss 3876  df-pss 3878  df-nul 4227  df-if 4422  df-pw 4497  df-sn 4524  df-pr 4526  df-tp 4528  df-op 4530  df-ot 4532  df-uni 4800  df-int 4840  df-iun 4886  df-iin 4887  df-br 5034  df-opab 5096  df-mpt 5114  df-tr 5140  df-id 5431  df-eprel 5436  df-po 5444  df-so 5445  df-fr 5484  df-se 5485  df-we 5486  df-xp 5531  df-rel 5532  df-cnv 5533  df-co 5534  df-dm 5535  df-rn 5536  df-res 5537  df-ima 5538  df-pred 6127  df-ord 6173  df-on 6174  df-lim 6175  df-suc 6176  df-iota 6295  df-fun 6338  df-fn 6339  df-f 6340  df-f1 6341  df-fo 6342  df-f1o 6343  df-fv 6344  df-isom 6345  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7406  df-om 7581  df-1st 7694  df-2nd 7695  df-supp 7837  df-wrecs 7958  df-recs 8019  df-rdg 8057  df-1o 8113  df-er 8300  df-map 8419  df-ixp 8481  df-en 8529  df-dom 8530  df-sdom 8531  df-fin 8532  df-fsupp 8868  df-sup 8940  df-oi 9008  df-card 9402  df-pnf 10716  df-mnf 10717  df-xr 10718  df-ltxr 10719  df-le 10720  df-sub 10911  df-neg 10912  df-nn 11676  df-2 11738  df-3 11739  df-4 11740  df-5 11741  df-6 11742  df-7 11743  df-8 11744  df-9 11745  df-n0 11936  df-z 12022  df-dec 12139  df-uz 12284  df-fz 12941  df-fzo 13084  df-seq 13420  df-hash 13742  df-struct 16544  df-ndx 16545  df-slot 16546  df-base 16548  df-sets 16549  df-ress 16550  df-plusg 16637  df-mulr 16638  df-sca 16640  df-vsca 16641  df-ip 16642  df-tset 16643  df-ple 16644  df-ds 16646  df-hom 16648  df-cco 16649  df-0g 16774  df-gsum 16775  df-prds 16780  df-pws 16782  df-mre 16916  df-mrc 16917  df-acs 16919  df-mgm 17919  df-sgrp 17968  df-mnd 17979  df-mhm 18023  df-submnd 18024  df-grp 18173  df-minusg 18174  df-sbg 18175  df-mulg 18293  df-subg 18344  df-ghm 18424  df-cntz 18515  df-cmn 18976  df-abl 18977  df-mgp 19309  df-ur 19321  df-ring 19368  df-subrg 19602  df-lmod 19705  df-lss 19773  df-sra 20013  df-rgmod 20014  df-dsmm 20498  df-frlm 20513  df-mamu 21087  df-mat 21109 This theorem is referenced by:  mat1rhm  21186
 Copyright terms: Public domain W3C validator