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	$Math input error$

Proof

Step	Hyp	Ref	Expression
1		eqid	$⊢ subringAlg (E) ({Base}_{K}) = subringAlg (E) ({Base}_{K})$
2		eqid	$⊢ subringAlg (E) ({Base}_{F}) = subringAlg (E) ({Base}_{F})$
3		eqid	$⊢ subringAlg (E ↾_{𝑠} {Base}_{F}) ({Base}_{K}) = subringAlg (E ↾_{𝑠} {Base}_{F}) ({Base}_{K})$
4		eqid	$⊢ E ↾_{𝑠} {Base}_{F} = E ↾_{𝑠} {Base}_{F}$
5		eqid	$⊢ E ↾_{𝑠} {Base}_{K} = E ↾_{𝑠} {Base}_{K}$
6		simpl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E /_{FldExt} F$
7		fldextfld1	$⊢ E /_{FldExt} F \to E \in Field$
8	6 7	syl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E \in Field$
9		isfld	$⊢ E \in Field \leftrightarrow (E \in DivRing \land E \in CRing)$
10	9	simplbi	$⊢ E \in Field \to E \in DivRing$
11	8 10	syl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E \in DivRing$
12		fldextfld1	$⊢ F /_{FldExt} K \to F \in Field$
13	12	adantl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to F \in Field$
14		brfldext	$⊢ (E \in Field \land F \in Field) \to (E /_{FldExt} F \leftrightarrow (F = E ↾_{𝑠} {Base}_{F} \land {Base}_{F} \in SubRing (E)))$
15	8 13 14	syl2anc	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to (E /_{FldExt} F \leftrightarrow (F = E ↾_{𝑠} {Base}_{F} \land {Base}_{F} \in SubRing (E)))$
16	6 15	mpbid	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to (F = E ↾_{𝑠} {Base}_{F} \land {Base}_{F} \in SubRing (E))$
17	16	simpld	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to F = E ↾_{𝑠} {Base}_{F}$
18		isfld	$⊢ F \in Field \leftrightarrow (F \in DivRing \land F \in CRing)$
19	18	simplbi	$⊢ F \in Field \to F \in DivRing$
20	13 19	syl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to F \in DivRing$
21	17 20	eqeltrrd	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E ↾_{𝑠} {Base}_{F} \in DivRing$
22		fldexttr	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E /_{FldExt} K$
23		fldextfld2	$⊢ F /_{FldExt} K \to K \in Field$
24	23	adantl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to K \in Field$
25		brfldext	$⊢ (E \in Field \land K \in Field) \to (E /_{FldExt} K \leftrightarrow (K = E ↾_{𝑠} {Base}_{K} \land {Base}_{K} \in SubRing (E)))$
26	8 24 25	syl2anc	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to (E /_{FldExt} K \leftrightarrow (K = E ↾_{𝑠} {Base}_{K} \land {Base}_{K} \in SubRing (E)))$
27	22 26	mpbid	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to (K = E ↾_{𝑠} {Base}_{K} \land {Base}_{K} \in SubRing (E))$
28	27	simpld	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to K = E ↾_{𝑠} {Base}_{K}$
29		isfld	$⊢ K \in Field \leftrightarrow (K \in DivRing \land K \in CRing)$
30	29	simplbi	$⊢ K \in Field \to K \in DivRing$
31	24 30	syl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to K \in DivRing$
32	28 31	eqeltrrd	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E ↾_{𝑠} {Base}_{K} \in DivRing$
33	16	simprd	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to {Base}_{F} \in SubRing (E)$
34		eqid	$⊢ {Base}_{K} = {Base}_{K}$
35	34	fldextsubrg	$⊢ F /_{FldExt} K \to {Base}_{K} \in SubRing (F)$
36	35	adantl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to {Base}_{K} \in SubRing (F)$
37	17	fveq2d	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to SubRing (F) = SubRing (E ↾_{𝑠} {Base}_{F})$
38	36 37	eleqtrd	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to {Base}_{K} \in SubRing (E ↾_{𝑠} {Base}_{F})$
39	1 2 3 4 5 11 21 32 33 38	fedgmul	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to \dim (subringAlg (E) ({Base}_{K})) = \dim (subringAlg (E) ({Base}_{F})) \cdot_{𝑒} \dim (subringAlg (E ↾_{𝑠} {Base}_{F}) ({Base}_{K}))$
40		extdgval	$⊢ E /_{FldExt} K \to E [. : .] K = \dim (subringAlg (E) ({Base}_{K}))$
41	22 40	syl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E [. : .] K = \dim (subringAlg (E) ({Base}_{K}))$
42		extdgval	$⊢ E /_{FldExt} F \to E [. : .] F = \dim (subringAlg (E) ({Base}_{F}))$
43	6 42	syl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to E [. : .] F = \dim (subringAlg (E) ({Base}_{F}))$
44		extdgval	$⊢ F /_{FldExt} K \to F [. : .] K = \dim (subringAlg (F) ({Base}_{K}))$
45	44	adantl	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to F [. : .] K = \dim (subringAlg (F) ({Base}_{K}))$
46	17	fveq2d	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to subringAlg (F) = subringAlg (E ↾_{𝑠} {Base}_{F})$
47	46	fveq1d	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to subringAlg (F) ({Base}_{K}) = subringAlg (E ↾_{𝑠} {Base}_{F}) ({Base}_{K})$
48	47	fveq2d	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to \dim (subringAlg (F) ({Base}_{K})) = \dim (subringAlg (E ↾_{𝑠} {Base}_{F}) ({Base}_{K}))$
49	45 48	eqtrd	$⊢ (E /_{FldExt} F \land F /_{FldExt} K) \to F [. : .] K = \dim (subringAlg (E ↾_{𝑠} {Base}_{F}) ({Base}_{K}))$
50	43 49	oveq12d	$Math input error$
51	39 41 50	3eqtr4d	$Math input error$

Metamath Proof Explorer

Theorem extdgmul

Proof