Theorem extdgval

Description: Value of the field extension degree operation. (Contributed by Thierry Arnoux, 29-Jul-2023)

	Ref	Expression
Assertion	extdgval	⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )

Proof

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 ‘ 𝐹 ) ) ) )