Metamath Proof Explorer

Theorem fldexttr

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

Ref Expression
Assertion fldexttr ⊢ E /FldExt F ∧ F /FldExt K → E /FldExt K

Proof

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