Step |
Hyp |
Ref |
Expression |
1 |
|
mat1rhmval.k |
⊢ 𝐾 = ( Base ‘ 𝑅 ) |
2 |
|
mat1rhmval.a |
⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 ) |
3 |
|
mat1rhmval.b |
⊢ 𝐵 = ( Base ‘ 𝐴 ) |
4 |
|
mat1rhmval.o |
⊢ 𝑂 = 〈 𝐸 , 𝐸 〉 |
5 |
|
mat1rhmval.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { 〈 𝑂 , 𝑥 〉 } ) |
6 |
|
simpl |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝑅 ∈ Ring ) |
7 |
|
snfi |
⊢ { 𝐸 } ∈ Fin |
8 |
2
|
matring |
⊢ ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring ) |
9 |
7 6 8
|
sylancr |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐴 ∈ Ring ) |
10 |
1 2 3 4 5
|
mat1ghm |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝐴 ) ) |
11 |
|
eqid |
⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 ) |
12 |
|
eqid |
⊢ ( mulGrp ‘ 𝐴 ) = ( mulGrp ‘ 𝐴 ) |
13 |
1 2 3 4 5 11 12
|
mat1mhm |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝐴 ) ) ) |
14 |
10 13
|
jca |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → ( 𝐹 ∈ ( 𝑅 GrpHom 𝐴 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝐴 ) ) ) ) |
15 |
11 12
|
isrhm |
⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝐴 ) ↔ ( ( 𝑅 ∈ Ring ∧ 𝐴 ∈ Ring ) ∧ ( 𝐹 ∈ ( 𝑅 GrpHom 𝐴 ) ∧ 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝐴 ) ) ) ) ) |
16 |
6 9 14 15
|
syl21anbrc |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑅 RingHom 𝐴 ) ) |