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→ 𝐵 ) |