Description: There is a ring isomorphism from a ring to 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 | mat1rngiso | ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑅 RingIso 𝐴 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | mat1rhmval.k | ⊢ 𝐾 = ( Base ‘ 𝑅 ) | |
2 | mat1rhmval.a | ⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 ) | |
3 | mat1rhmval.b | ⊢ 𝐵 = ( Base ‘ 𝐴 ) | |
4 | mat1rhmval.o | ⊢ 𝑂 = 〈 𝐸 , 𝐸 〉 | |
5 | mat1rhmval.f | ⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { 〈 𝑂 , 𝑥 〉 } ) | |
6 | 1 2 3 4 5 | mat1rhm | ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑅 RingHom 𝐴 ) ) |
7 | 1 2 3 4 5 | mat1f1o | ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 : 𝐾 –1-1-onto→ 𝐵 ) |
8 | 1 3 | isrim | ⊢ ( 𝐹 ∈ ( 𝑅 RingIso 𝐴 ) ↔ ( 𝐹 ∈ ( 𝑅 RingHom 𝐴 ) ∧ 𝐹 : 𝐾 –1-1-onto→ 𝐵 ) ) |
9 | 6 7 8 | sylanbrc | ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 ∈ ( 𝑅 RingIso 𝐴 ) ) |