Step |
Hyp |
Ref |
Expression |
0 |
|
cextdg |
⊢ [:] |
1 |
|
ve |
⊢ 𝑒 |
2 |
|
cvv |
⊢ V |
3 |
|
vf |
⊢ 𝑓 |
4 |
|
cfldext |
⊢ /FldExt |
5 |
1
|
cv |
⊢ 𝑒 |
6 |
5
|
csn |
⊢ { 𝑒 } |
7 |
4 6
|
cima |
⊢ ( /FldExt “ { 𝑒 } ) |
8 |
|
cldim |
⊢ dim |
9 |
|
csra |
⊢ subringAlg |
10 |
5 9
|
cfv |
⊢ ( subringAlg ‘ 𝑒 ) |
11 |
|
cbs |
⊢ Base |
12 |
3
|
cv |
⊢ 𝑓 |
13 |
12 11
|
cfv |
⊢ ( Base ‘ 𝑓 ) |
14 |
13 10
|
cfv |
⊢ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) |
15 |
14 8
|
cfv |
⊢ ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) |
16 |
1 3 2 7 15
|
cmpo |
⊢ ( 𝑒 ∈ V , 𝑓 ∈ ( /FldExt “ { 𝑒 } ) ↦ ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) ) |
17 |
0 16
|
wceq |
⊢ [:] = ( 𝑒 ∈ V , 𝑓 ∈ ( /FldExt “ { 𝑒 } ) ↦ ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) ) |