Metamath Proof Explorer


Theorem mat1ric

Description: A ring is isomorphic to the ring of matrices with dimension 1 over this ring. (Contributed by AV, 30-Dec-2019)

Ref Expression
Hypothesis mat1ric.a 𝐴 = ( { 𝐸 } Mat 𝑅 )
Assertion mat1ric ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → 𝑅𝑟 𝐴 )

Proof

Step Hyp Ref Expression
1 mat1ric.a 𝐴 = ( { 𝐸 } Mat 𝑅 )
2 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
3 eqid ( Base ‘ 𝐴 ) = ( Base ‘ 𝐴 )
4 eqid 𝐸 , 𝐸 ⟩ = ⟨ 𝐸 , 𝐸
5 opeq2 ( 𝑥 = 𝑦 → ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑥 ⟩ = ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑦 ⟩ )
6 5 sneqd ( 𝑥 = 𝑦 → { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑥 ⟩ } = { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑦 ⟩ } )
7 6 cbvmptv ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑥 ⟩ } ) = ( 𝑦 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑦 ⟩ } )
8 2 1 3 4 7 mat1rngiso ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → ( 𝑥 ∈ ( Base ‘ 𝑅 ) ↦ { ⟨ ⟨ 𝐸 , 𝐸 ⟩ , 𝑥 ⟩ } ) ∈ ( 𝑅 RingIso 𝐴 ) )
9 8 ne0d ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → ( 𝑅 RingIso 𝐴 ) ≠ ∅ )
10 brric ( 𝑅𝑟 𝐴 ↔ ( 𝑅 RingIso 𝐴 ) ≠ ∅ )
11 9 10 sylibr ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → 𝑅𝑟 𝐴 )