Theorem extdgmul

Description: The multiplicativity formula for degrees of field extensions. Given E a field extension of F , itself a field extension of K , the degree of the extension E /FldExt K is the product of the degrees of the extensions E /FldExt F and F /FldExt K . Proposition 1.2 of Lang, p. 224. (Contributed by Thierry Arnoux, 30-Jul-2023)

	Ref	Expression
Assertion	extdgmul	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 [:] 𝐾 ) = ( ( 𝐸 [:] 𝐹 ) ·e ( 𝐹 [:] 𝐾 ) ) )

Proof

Step	Hyp	Ref	Expression
1		eqid	⊢ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐾 ) ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐾 ) )
2		eqid	⊢ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) = ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) )
3		eqid	⊢ ( ( subringAlg ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) ‘ ( Base ‘ 𝐾 ) ) = ( ( subringAlg ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) ‘ ( Base ‘ 𝐾 ) )
4		eqid	⊢ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) = ( 𝐸 ↾s ( Base ‘ 𝐹 ) )
5		eqid	⊢ ( 𝐸 ↾s ( Base ‘ 𝐾 ) ) = ( 𝐸 ↾s ( Base ‘ 𝐾 ) )
6		simpl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐸 /FldExt 𝐹 )
7		fldextfld1	⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ Field )
8	6 7	syl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐸 ∈ Field )
9		isfld	⊢ ( 𝐸 ∈ Field ↔ ( 𝐸 ∈ DivRing ∧ 𝐸 ∈ CRing ) )
10	9	simplbi	⊢ ( 𝐸 ∈ Field → 𝐸 ∈ DivRing )
11	8 10	syl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐸 ∈ DivRing )
12		fldextfld1	⊢ ( 𝐹 /FldExt 𝐾 → 𝐹 ∈ Field )
13	12	adantl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐹 ∈ Field )
14		brfldext	⊢ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ Field ) → ( 𝐸 /FldExt 𝐹 ↔ ( 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ) )
15	8 13 14	syl2anc	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 /FldExt 𝐹 ↔ ( 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ) )
16	6 15	mpbid	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) )
17	16	simpld	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) )
18		isfld	⊢ ( 𝐹 ∈ Field ↔ ( 𝐹 ∈ DivRing ∧ 𝐹 ∈ CRing ) )
19	18	simplbi	⊢ ( 𝐹 ∈ Field → 𝐹 ∈ DivRing )
20	13 19	syl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐹 ∈ DivRing )
21	17 20	eqeltrrd	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∈ DivRing )
22		fldexttr	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐸 /FldExt 𝐾 )
23		fldextfld2	⊢ ( 𝐹 /FldExt 𝐾 → 𝐾 ∈ Field )
24	23	adantl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐾 ∈ Field )
25		brfldext	⊢ ( ( 𝐸 ∈ Field ∧ 𝐾 ∈ Field ) → ( 𝐸 /FldExt 𝐾 ↔ ( 𝐾 = ( 𝐸 ↾s ( Base ‘ 𝐾 ) ) ∧ ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐸 ) ) ) )
26	8 24 25	syl2anc	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 /FldExt 𝐾 ↔ ( 𝐾 = ( 𝐸 ↾s ( Base ‘ 𝐾 ) ) ∧ ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐸 ) ) ) )
27	22 26	mpbid	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐾 = ( 𝐸 ↾s ( Base ‘ 𝐾 ) ) ∧ ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐸 ) ) )
28	27	simpld	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐾 = ( 𝐸 ↾s ( Base ‘ 𝐾 ) ) )
29		isfld	⊢ ( 𝐾 ∈ Field ↔ ( 𝐾 ∈ DivRing ∧ 𝐾 ∈ CRing ) )
30	29	simplbi	⊢ ( 𝐾 ∈ Field → 𝐾 ∈ DivRing )
31	24 30	syl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐾 ∈ DivRing )
32	28 31	eqeltrrd	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 ↾s ( Base ‘ 𝐾 ) ) ∈ DivRing )
33	16	simprd	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) )
34		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
35	34	fldextsubrg	⊢ ( 𝐹 /FldExt 𝐾 → ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐹 ) )
36	35	adantl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐹 ) )
37	17	fveq2d	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( SubRing ‘ 𝐹 ) = ( SubRing ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) )
38	36 37	eleqtrd	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) )
39	1 2 3 4 5 11 21 32 33 38	fedgmul	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐾 ) ) ) = ( ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ·e ( dim ‘ ( ( subringAlg ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) ‘ ( Base ‘ 𝐾 ) ) ) ) )
40		extdgval	⊢ ( 𝐸 /FldExt 𝐾 → ( 𝐸 [:] 𝐾 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐾 ) ) ) )
41	22 40	syl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 [:] 𝐾 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐾 ) ) ) )
42		extdgval	⊢ ( 𝐸 /FldExt 𝐹 → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
43	6 42	syl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 [:] 𝐹 ) = ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) )
44		extdgval	⊢ ( 𝐹 /FldExt 𝐾 → ( 𝐹 [:] 𝐾 ) = ( dim ‘ ( ( subringAlg ‘ 𝐹 ) ‘ ( Base ‘ 𝐾 ) ) ) )
45	44	adantl	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐹 [:] 𝐾 ) = ( dim ‘ ( ( subringAlg ‘ 𝐹 ) ‘ ( Base ‘ 𝐾 ) ) ) )
46	17	fveq2d	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( subringAlg ‘ 𝐹 ) = ( subringAlg ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) )
47	46	fveq1d	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( ( subringAlg ‘ 𝐹 ) ‘ ( Base ‘ 𝐾 ) ) = ( ( subringAlg ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) ‘ ( Base ‘ 𝐾 ) ) )
48	47	fveq2d	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( dim ‘ ( ( subringAlg ‘ 𝐹 ) ‘ ( Base ‘ 𝐾 ) ) ) = ( dim ‘ ( ( subringAlg ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) ‘ ( Base ‘ 𝐾 ) ) ) )
49	45 48	eqtrd	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐹 [:] 𝐾 ) = ( dim ‘ ( ( subringAlg ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) ‘ ( Base ‘ 𝐾 ) ) ) )
50	43 49	oveq12d	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( ( 𝐸 [:] 𝐹 ) ·e ( 𝐹 [:] 𝐾 ) ) = ( ( dim ‘ ( ( subringAlg ‘ 𝐸 ) ‘ ( Base ‘ 𝐹 ) ) ) ·e ( dim ‘ ( ( subringAlg ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) ‘ ( Base ‘ 𝐾 ) ) ) ) )
51	39 41 50	3eqtr4d	⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 [:] 𝐾 ) = ( ( 𝐸 [:] 𝐹 ) ·e ( 𝐹 [:] 𝐾 ) ) )