Metamath Proof Explorer

Theorem fldexttr

Description: Field extension is a transitive relation. (Contributed by Thierry Arnoux, 29-Jul-2023)

Ref Expression
Assertion fldexttr ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐸 /FldExt 𝐾 )

Proof

Step Hyp Ref Expression
1 simpr ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐹 /FldExt 𝐾 )
2 simpl ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐸 /FldExt 𝐹 )
3 fldextfld2 ⊢ ( 𝐸 /FldExt 𝐹 → 𝐹 ∈ Field )
4 2 3 syl ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐹 ∈ Field )
5 fldextfld2 ⊢ ( 𝐹 /FldExt 𝐾 → 𝐾 ∈ Field )
6 1 5 syl ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐾 ∈ Field )
7 brfldext ⊢ ( ( 𝐹 ∈ Field ∧ 𝐾 ∈ Field ) → ( 𝐹 /FldExt 𝐾 ↔ ( 𝐾 = ( 𝐹 ↾s ( Base ‘ 𝐾 ) ) ∧ ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐹 ) ) ) )
8 4 6 7 syl2anc ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐹 /FldExt 𝐾 ↔ ( 𝐾 = ( 𝐹 ↾s ( Base ‘ 𝐾 ) ) ∧ ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐹 ) ) ) )
9 1 8 mpbid ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐾 = ( 𝐹 ↾s ( Base ‘ 𝐾 ) ) ∧ ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐹 ) ) )
10 9 simpld ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐾 = ( 𝐹 ↾s ( Base ‘ 𝐾 ) ) )
11 fldextfld1 ⊢ ( 𝐸 /FldExt 𝐹 → 𝐸 ∈ Field )
12 2 11 syl ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐸 ∈ Field )
13 brfldext ⊢ ( ( 𝐸 ∈ Field ∧ 𝐹 ∈ Field ) → ( 𝐸 /FldExt 𝐹 ↔ ( 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ) )
14 12 4 13 syl2anc ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 /FldExt 𝐹 ↔ ( 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) ) )
15 2 14 mpbid ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ∧ ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ) )
16 15 simpld ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐹 = ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) )
17 16 oveq1d ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐹 ↾s ( Base ‘ 𝐾 ) ) = ( ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ↾s ( Base ‘ 𝐾 ) ) )
18 fvex ⊢ ( Base ‘ 𝐹 ) ∈ V
19 fvex ⊢ ( Base ‘ 𝐾 ) ∈ V
20 ressress ⊢ ( ( ( Base ‘ 𝐹 ) ∈ V ∧ ( Base ‘ 𝐾 ) ∈ V ) → ( ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ↾s ( Base ‘ 𝐾 ) ) = ( 𝐸 ↾s ( ( Base ‘ 𝐹 ) ∩ ( Base ‘ 𝐾 ) ) ) )
21 18 19 20 mp2an ⊢ ( ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ↾s ( Base ‘ 𝐾 ) ) = ( 𝐸 ↾s ( ( Base ‘ 𝐹 ) ∩ ( Base ‘ 𝐾 ) ) )
22 17 21 eqtrdi ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐹 ↾s ( Base ‘ 𝐾 ) ) = ( 𝐸 ↾s ( ( Base ‘ 𝐹 ) ∩ ( Base ‘ 𝐾 ) ) ) )
23 incom ⊢ ( ( Base ‘ 𝐾 ) ∩ ( Base ‘ 𝐹 ) ) = ( ( Base ‘ 𝐹 ) ∩ ( Base ‘ 𝐾 ) )
24 9 simprd ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐹 ) )
25 eqid ⊢ ( Base ‘ 𝐹 ) = ( Base ‘ 𝐹 )
26 25 subrgss ⊢ ( ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐹 ) → ( Base ‘ 𝐾 ) ⊆ ( Base ‘ 𝐹 ) )
27 24 26 syl ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( Base ‘ 𝐾 ) ⊆ ( Base ‘ 𝐹 ) )
28 dfss2 ⊢ ( ( Base ‘ 𝐾 ) ⊆ ( Base ‘ 𝐹 ) ↔ ( ( Base ‘ 𝐾 ) ∩ ( Base ‘ 𝐹 ) ) = ( Base ‘ 𝐾 ) )
29 27 28 sylib ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( ( Base ‘ 𝐾 ) ∩ ( Base ‘ 𝐹 ) ) = ( Base ‘ 𝐾 ) )
30 23 29 eqtr3id ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( ( Base ‘ 𝐹 ) ∩ ( Base ‘ 𝐾 ) ) = ( Base ‘ 𝐾 ) )
31 30 oveq2d ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 ↾s ( ( Base ‘ 𝐹 ) ∩ ( Base ‘ 𝐾 ) ) ) = ( 𝐸 ↾s ( Base ‘ 𝐾 ) ) )
32 10 22 31 3eqtrd ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐾 = ( 𝐸 ↾s ( Base ‘ 𝐾 ) ) )
33 15 simprd ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) )
34 16 fveq2d ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( SubRing ‘ 𝐹 ) = ( SubRing ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) )
35 24 34 eleqtrd ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) )
36 eqid ⊢ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) = ( 𝐸 ↾s ( Base ‘ 𝐹 ) )
37 36 subsubrg ⊢ ( ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) → ( ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) ↔ ( ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐸 ) ∧ ( Base ‘ 𝐾 ) ⊆ ( Base ‘ 𝐹 ) ) ) )
38 37 simprbda ⊢ ( ( ( Base ‘ 𝐹 ) ∈ ( SubRing ‘ 𝐸 ) ∧ ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ ( 𝐸 ↾s ( Base ‘ 𝐹 ) ) ) ) → ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐸 ) )
39 33 35 38 syl2anc ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐸 ) )
40 brfldext ⊢ ( ( 𝐸 ∈ Field ∧ 𝐾 ∈ Field ) → ( 𝐸 /FldExt 𝐾 ↔ ( 𝐾 = ( 𝐸 ↾s ( Base ‘ 𝐾 ) ) ∧ ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐸 ) ) ) )
41 12 6 40 syl2anc ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → ( 𝐸 /FldExt 𝐾 ↔ ( 𝐾 = ( 𝐸 ↾s ( Base ‘ 𝐾 ) ) ∧ ( Base ‘ 𝐾 ) ∈ ( SubRing ‘ 𝐸 ) ) ) )
42 32 39 41 mpbir2and ⊢ ( ( 𝐸 /FldExt 𝐹 ∧ 𝐹 /FldExt 𝐾 ) → 𝐸 /FldExt 𝐾 )