Step |
Hyp |
Ref |
Expression |
1 |
|
mat1rhmval.k |
⊢ 𝐾 = ( Base ‘ 𝑅 ) |
2 |
|
mat1rhmval.a |
⊢ 𝐴 = ( { 𝐸 } Mat 𝑅 ) |
3 |
|
mat1rhmval.b |
⊢ 𝐵 = ( Base ‘ 𝐴 ) |
4 |
|
mat1rhmval.o |
⊢ 𝑂 = 〈 𝐸 , 𝐸 〉 |
5 |
|
mat1rhmval.f |
⊢ 𝐹 = ( 𝑥 ∈ 𝐾 ↦ { 〈 𝑂 , 𝑥 〉 } ) |
6 |
|
opeq2 |
⊢ ( 𝑥 = 𝑋 → 〈 𝑂 , 𝑥 〉 = 〈 𝑂 , 𝑋 〉 ) |
7 |
6
|
sneqd |
⊢ ( 𝑥 = 𝑋 → { 〈 𝑂 , 𝑥 〉 } = { 〈 𝑂 , 𝑋 〉 } ) |
8 |
|
simp3 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → 𝑋 ∈ 𝐾 ) |
9 |
|
snex |
⊢ { 〈 𝑂 , 𝑋 〉 } ∈ V |
10 |
9
|
a1i |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → { 〈 𝑂 , 𝑋 〉 } ∈ V ) |
11 |
5 7 8 10
|
fvmptd3 |
⊢ ( ( 𝑅 ∈ Ring ∧ 𝐸 ∈ 𝑉 ∧ 𝑋 ∈ 𝐾 ) → ( 𝐹 ‘ 𝑋 ) = { 〈 𝑂 , 𝑋 〉 } ) |