Metamath Proof Explorer

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 ⊢ E /FldExt F ∧ F /FldExt K → E .:. K = E : F ⋅ 𝑒 F : K

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 ∧ F /FldExt K → E /FldExt F
7 fldextfld1 ⊢ E /FldExt F → E ∈ Field
8 6 7 syl ⊢ E /FldExt F ∧ F /FldExt K → E ∈ Field
9 isfld ⊢ E ∈ Field ↔ E ∈ DivRing ∧ E ∈ CRing
10 9 simplbi ⊢ E ∈ Field → E ∈ DivRing
11 8 10 syl ⊢ E /FldExt F ∧ F /FldExt K → E ∈ DivRing
12 fldextfld1 ⊢ F /FldExt K → F ∈ Field
13 12 adantl ⊢ E /FldExt F ∧ F /FldExt K → F ∈ Field
14 brfldext ⊢ E ∈ Field ∧ F ∈ Field → E /FldExt F ↔ F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E
15 8 13 14 syl2anc ⊢ E /FldExt F ∧ F /FldExt K → E /FldExt F ↔ F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E
16 6 15 mpbid ⊢ E /FldExt F ∧ F /FldExt K → F = E ↾ 𝑠 Base F ∧ Base F ∈ SubRing ⁡ E
17 16 simpld ⊢ E /FldExt F ∧ F /FldExt K → F = E ↾ 𝑠 Base F
18 isfld ⊢ F ∈ Field ↔ F ∈ DivRing ∧ F ∈ CRing
19 18 simplbi ⊢ F ∈ Field → F ∈ DivRing
20 13 19 syl ⊢ E /FldExt F ∧ F /FldExt K → F ∈ DivRing
21 17 20 eqeltrrd ⊢ E /FldExt F ∧ F /FldExt K → E ↾ 𝑠 Base F ∈ DivRing
22 fldexttr ⊢ E /FldExt F ∧ F /FldExt K → E /FldExt K
23 fldextfld2 ⊢ F /FldExt K → K ∈ Field
24 23 adantl ⊢ E /FldExt F ∧ F /FldExt K → K ∈ Field
25 brfldext ⊢ E ∈ Field ∧ K ∈ Field → E /FldExt K ↔ K = E ↾ 𝑠 Base K ∧ Base K ∈ SubRing ⁡ E
26 8 24 25 syl2anc ⊢ E /FldExt F ∧ F /FldExt K → E /FldExt K ↔ K = E ↾ 𝑠 Base K ∧ Base K ∈ SubRing ⁡ E
27 22 26 mpbid ⊢ E /FldExt F ∧ F /FldExt K → K = E ↾ 𝑠 Base K ∧ Base K ∈ SubRing ⁡ E
28 27 simpld ⊢ E /FldExt F ∧ F /FldExt K → K = E ↾ 𝑠 Base K
29 isfld ⊢ K ∈ Field ↔ K ∈ DivRing ∧ K ∈ CRing
30 29 simplbi ⊢ K ∈ Field → K ∈ DivRing
31 24 30 syl ⊢ E /FldExt F ∧ F /FldExt K → K ∈ DivRing
32 28 31 eqeltrrd ⊢ E /FldExt F ∧ F /FldExt K → E ↾ 𝑠 Base K ∈ DivRing
33 16 simprd ⊢ E /FldExt F ∧ F /FldExt K → Base F ∈ SubRing ⁡ E
34 eqid ⊢ Base K = Base K
35 34 fldextsubrg ⊢ F /FldExt K → Base K ∈ SubRing ⁡ F
36 35 adantl ⊢ E /FldExt F ∧ F /FldExt K → Base K ∈ SubRing ⁡ F
37 17 fveq2d ⊢ E /FldExt F ∧ F /FldExt K → SubRing ⁡ F = SubRing ⁡ E ↾ 𝑠 Base F
38 36 37 eleqtrd ⊢ E /FldExt F ∧ F /FldExt K → Base K ∈ SubRing ⁡ E ↾ 𝑠 Base F
39 1 2 3 4 5 11 21 32 33 38 fedgmul ⊢ E /FldExt F ∧ F /FldExt K → dim ⁡ subringAlg ⁡ E ⁡ Base K = dim ⁡ subringAlg ⁡ E ⁡ Base F ⋅ 𝑒 dim ⁡ subringAlg ⁡ E ↾ 𝑠 Base F ⁡ Base K
40 extdgval ⊢ E /FldExt K → E .:. K = dim ⁡ subringAlg ⁡ E ⁡ Base K
41 22 40 syl ⊢ E /FldExt F ∧ F /FldExt K → E .:. K = dim ⁡ subringAlg ⁡ E ⁡ Base K
42 extdgval ⊢ E /FldExt F → E .:. F = dim ⁡ subringAlg ⁡ E ⁡ Base F
43 6 42 syl ⊢ E /FldExt F ∧ F /FldExt K → E .:. F = dim ⁡ subringAlg ⁡ E ⁡ Base F
44 extdgval ⊢ F /FldExt K → F .:. K = dim ⁡ subringAlg ⁡ F ⁡ Base K
45 44 adantl ⊢ E /FldExt F ∧ F /FldExt K → F .:. K = dim ⁡ subringAlg ⁡ F ⁡ Base K
46 17 fveq2d ⊢ E /FldExt F ∧ F /FldExt K → subringAlg ⁡ F = subringAlg ⁡ E ↾ 𝑠 Base F
47 46 fveq1d ⊢ E /FldExt F ∧ F /FldExt K → subringAlg ⁡ F ⁡ Base K = subringAlg ⁡ E ↾ 𝑠 Base F ⁡ Base K
48 47 fveq2d ⊢ E /FldExt F ∧ F /FldExt K → dim ⁡ subringAlg ⁡ F ⁡ Base K = dim ⁡ subringAlg ⁡ E ↾ 𝑠 Base F ⁡ Base K
49 45 48 eqtrd ⊢ E /FldExt F ∧ F /FldExt K → F .:. K = dim ⁡ subringAlg ⁡ E ↾ 𝑠 Base F ⁡ Base K
50 43 49 oveq12d ⊢ E /FldExt F ∧ F /FldExt K → E : F ⋅ 𝑒 F : K = dim ⁡ subringAlg ⁡ E ⁡ Base F ⋅ 𝑒 dim ⁡ subringAlg ⁡ E ↾ 𝑠 Base F ⁡ Base K
51 39 41 50 3eqtr4d ⊢ E /FldExt F ∧ F /FldExt K → E .:. K = E : F ⋅ 𝑒 F : K