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 ( ( 𝐸 /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 ( 𝐹 [:] 𝐾 ) ) )