Description: There is a function 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 | mat1f | ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 : 𝐾 ⟶ 𝐵 ) |
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 | mat1f1o | ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 : 𝐾 –1-1-onto→ 𝐵 ) |
7 | f1of | ⊢ ( 𝐹 : 𝐾 –1-1-onto→ 𝐵 → 𝐹 : 𝐾 ⟶ 𝐵 ) | |
8 | 6 7 | syl | ⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ) → 𝐹 : 𝐾 ⟶ 𝐵 ) |