Metamath Proof Explorer


Theorem mat1f1o

Description: There is a 1-1 function from a ring onto 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 mat1f1o ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → 𝐹 : 𝐾1-1-onto𝐵 )

Proof

Step Hyp Ref Expression
1 mat1rhmval.k 𝐾 = ( Base ‘ 𝑅 )
2 mat1rhmval.a 𝐴 = ( { 𝐸 } Mat 𝑅 )
3 mat1rhmval.b 𝐵 = ( Base ‘ 𝐴 )
4 mat1rhmval.o 𝑂 = ⟨ 𝐸 , 𝐸
5 mat1rhmval.f 𝐹 = ( 𝑥𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } )
6 1 fvexi 𝐾 ∈ V
7 opex 𝐸 , 𝐸 ⟩ ∈ V
8 4 7 eqeltri 𝑂 ∈ V
9 6 8 pm3.2i ( 𝐾 ∈ V ∧ 𝑂 ∈ V )
10 vex 𝑥 ∈ V
11 8 10 xpsn ( { 𝑂 } × { 𝑥 } ) = { ⟨ 𝑂 , 𝑥 ⟩ }
12 11 eqcomi { ⟨ 𝑂 , 𝑥 ⟩ } = ( { 𝑂 } × { 𝑥 } )
13 12 mpteq2i ( 𝑥𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } ) = ( 𝑥𝐾 ↦ ( { 𝑂 } × { 𝑥 } ) )
14 13 mapsnf1o ( ( 𝐾 ∈ V ∧ 𝑂 ∈ V ) → ( 𝑥𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } ) : 𝐾1-1-onto→ ( 𝐾m { 𝑂 } ) )
15 9 14 mp1i ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → ( 𝑥𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } ) : 𝐾1-1-onto→ ( 𝐾m { 𝑂 } ) )
16 5 a1i ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → 𝐹 = ( 𝑥𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } ) )
17 eqidd ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → 𝐾 = 𝐾 )
18 4 sneqi { 𝑂 } = { ⟨ 𝐸 , 𝐸 ⟩ }
19 simpr ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → 𝐸𝑉 )
20 xpsng ( ( 𝐸𝑉𝐸𝑉 ) → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
21 19 20 sylancom ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → ( { 𝐸 } × { 𝐸 } ) = { ⟨ 𝐸 , 𝐸 ⟩ } )
22 18 21 eqtr4id ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → { 𝑂 } = ( { 𝐸 } × { 𝐸 } ) )
23 22 oveq2d ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → ( 𝐾m { 𝑂 } ) = ( 𝐾m ( { 𝐸 } × { 𝐸 } ) ) )
24 snfi { 𝐸 } ∈ Fin
25 simpl ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → 𝑅 ∈ Ring )
26 2 1 matbas2 ( ( { 𝐸 } ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐾m ( { 𝐸 } × { 𝐸 } ) ) = ( Base ‘ 𝐴 ) )
27 24 25 26 sylancr ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → ( 𝐾m ( { 𝐸 } × { 𝐸 } ) ) = ( Base ‘ 𝐴 ) )
28 23 27 eqtrd ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → ( 𝐾m { 𝑂 } ) = ( Base ‘ 𝐴 ) )
29 3 28 eqtr4id ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → 𝐵 = ( 𝐾m { 𝑂 } ) )
30 16 17 29 f1oeq123d ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → ( 𝐹 : 𝐾1-1-onto𝐵 ↔ ( 𝑥𝐾 ↦ { ⟨ 𝑂 , 𝑥 ⟩ } ) : 𝐾1-1-onto→ ( 𝐾m { 𝑂 } ) ) )
31 15 30 mpbird ( ( 𝑅 ∈ Ring ∧ 𝐸𝑉 ) → 𝐹 : 𝐾1-1-onto𝐵 )