Step |
Hyp |
Ref |
Expression |
1 |
|
relfldext |
⊢ Rel /FldExt |
2 |
1
|
brrelex1i |
⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ V ) |
3 |
|
elrelimasn |
⊢ ( Rel /FldExt → ( 𝐹 ∈ ( /FldExt “ { 𝐸 } ) ↔ 𝐸 /FldExt 𝐹 ) ) |
4 |
1 3
|
ax-mp |
⊢ ( 𝐹 ∈ ( /FldExt “ { 𝐸 } ) ↔ 𝐸 /FldExt 𝐹 ) |
5 |
4
|
biimpri |
⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 ∈ ( /FldExt “ { 𝐸 } ) ) |
6 |
|
fvexd |
⊢ ( 𝐸 /FldExt 𝐹 → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ∈ V ) |
7 |
|
simpl |
⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → 𝑒 = 𝐸 ) |
8 |
7
|
fveq2d |
⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( subringAlg ‘ 𝑒 ) = ( subringAlg ‘ 𝐸 ) ) |
9 |
|
simpr |
⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → 𝑓 = 𝐹 ) |
10 |
9
|
fveq2d |
⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( Base ‘ 𝑓 ) = ( Base ‘ 𝐹 ) ) |
11 |
8 10
|
fveq12d |
⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) |
12 |
11
|
fveq2d |
⊢ ( ( 𝑒 = 𝐸 ∧ 𝑓 = 𝐹 ) → ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) |
13 |
|
sneq |
⊢ ( 𝑒 = 𝐸 → { 𝑒 } = { 𝐸 } ) |
14 |
13
|
imaeq2d |
⊢ ( 𝑒 = 𝐸 → ( /FldExt “ { 𝑒 } ) = ( /FldExt “ { 𝐸 } ) ) |
15 |
|
df-extdg |
⊢ [:] = ( 𝑒 ∈ V , 𝑓 ∈ ( /FldExt “ { 𝑒 } ) ↦ ( dim ‘ ( ( subringAlg ‘ 𝑒 ) ‘ ( Base ‘ 𝑓 ) ) ) ) |
16 |
12 14 15
|
ovmpox |
⊢ ( ( 𝐸 ∈ V ∧ 𝐹 ∈ ( /FldExt “ { 𝐸 } ) ∧ ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ∈ V ) → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) |
17 |
2 5 6 16
|
syl3anc |
⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ) |