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 e. Field )
4 2 3 syl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> F e. Field )
5 fldextfld2 
 |-  ( F /FldExt K -> K e. Field )
6 1 5 syl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> K e. Field )
7 brfldext 
 |-  ( ( F e. Field /\ K e. Field ) -> ( F /FldExt K <-> ( K = ( F |`s ( Base ` K ) ) /\ ( Base ` K ) e. ( SubRing ` F ) ) ) )
8 4 6 7 syl2anc 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( F /FldExt K <-> ( K = ( F |`s ( Base ` K ) ) /\ ( Base ` K ) e. ( SubRing ` F ) ) ) )
9 1 8 mpbid 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( K = ( F |`s ( Base ` K ) ) /\ ( Base ` K ) e. ( SubRing ` F ) ) )
10 9 simpld 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> K = ( F |`s ( Base ` K ) ) )
11 fldextfld1 
 |-  ( E /FldExt F -> E e. Field )
12 2 11 syl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> E e. Field )
13 brfldext 
 |-  ( ( E e. Field /\ F e. Field ) -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )
14 12 4 13 syl2anc 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E /FldExt F <-> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) ) )
15 2 14 mpbid 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( F = ( E |`s ( Base ` F ) ) /\ ( Base ` F ) e. ( SubRing ` E ) ) )
16 15 simpld 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> F = ( E |`s ( Base ` F ) ) )
17 16 oveq1d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( F |`s ( Base ` K ) ) = ( ( E |`s ( Base ` F ) ) |`s ( Base ` K ) ) )
18 fvex 
 |-  ( Base ` F ) e. _V
19 fvex 
 |-  ( Base ` K ) e. _V
20 ressress 
 |-  ( ( ( Base ` F ) e. _V /\ ( Base ` K ) e. _V ) -> ( ( E |`s ( Base ` F ) ) |`s ( Base ` K ) ) = ( E |`s ( ( Base ` F ) i^i ( Base ` K ) ) ) )
21 18 19 20 mp2an 
 |-  ( ( E |`s ( Base ` F ) ) |`s ( Base ` K ) ) = ( E |`s ( ( Base ` F ) i^i ( Base ` K ) ) )
22 17 21 eqtrdi 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( F |`s ( Base ` K ) ) = ( E |`s ( ( Base ` F ) i^i ( Base ` K ) ) ) )
23 incom 
 |-  ( ( Base ` K ) i^i ( Base ` F ) ) = ( ( Base ` F ) i^i ( Base ` K ) )
24 9 simprd 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( Base ` K ) e. ( SubRing ` F ) )
25 eqid 
 |-  ( Base ` F ) = ( Base ` F )
26 25 subrgss 
 |-  ( ( Base ` K ) e. ( SubRing ` F ) -> ( Base ` K ) C_ ( Base ` F ) )
27 24 26 syl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( Base ` K ) C_ ( Base ` F ) )
28 df-ss 
 |-  ( ( Base ` K ) C_ ( Base ` F ) <-> ( ( Base ` K ) i^i ( Base ` F ) ) = ( Base ` K ) )
29 27 28 sylib 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( ( Base ` K ) i^i ( Base ` F ) ) = ( Base ` K ) )
30 23 29 eqtr3id 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( ( Base ` F ) i^i ( Base ` K ) ) = ( Base ` K ) )
31 30 oveq2d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E |`s ( ( Base ` F ) i^i ( Base ` K ) ) ) = ( E |`s ( Base ` K ) ) )
32 10 22 31 3eqtrd 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> K = ( E |`s ( Base ` K ) ) )
33 15 simprd 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( Base ` F ) e. ( SubRing ` E ) )
34 16 fveq2d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( SubRing ` F ) = ( SubRing ` ( E |`s ( Base ` F ) ) ) )
35 24 34 eleqtrd 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( Base ` K ) e. ( SubRing ` ( E |`s ( Base ` F ) ) ) )
36 eqid 
 |-  ( E |`s ( Base ` F ) ) = ( E |`s ( Base ` F ) )
37 36 subsubrg 
 |-  ( ( Base ` F ) e. ( SubRing ` E ) -> ( ( Base ` K ) e. ( SubRing ` ( E |`s ( Base ` F ) ) ) <-> ( ( Base ` K ) e. ( SubRing ` E ) /\ ( Base ` K ) C_ ( Base ` F ) ) ) )
38 37 simprbda 
 |-  ( ( ( Base ` F ) e. ( SubRing ` E ) /\ ( Base ` K ) e. ( SubRing ` ( E |`s ( Base ` F ) ) ) ) -> ( Base ` K ) e. ( SubRing ` E ) )
39 33 35 38 syl2anc 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( Base ` K ) e. ( SubRing ` E ) )
40 brfldext 
 |-  ( ( E e. Field /\ K e. Field ) -> ( E /FldExt K <-> ( K = ( E |`s ( Base ` K ) ) /\ ( Base ` K ) e. ( SubRing ` E ) ) ) )
41 12 6 40 syl2anc 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E /FldExt K <-> ( K = ( E |`s ( Base ` K ) ) /\ ( Base ` K ) e. ( SubRing ` E ) ) ) )
42 32 39 41 mpbir2and 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> E /FldExt K )