This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem finexttrb

Description: The extension E of K is finite if and only if E is finite over F and F is finite over K . Corollary 1.3 of Lang , p. 225. (Contributed by Thierry Arnoux, 30-Jul-2023)

Ref Expression
Assertion finexttrb 
|- ( ( E /FldExt F /\ F /FldExt K ) -> ( E /FinExt K <-> ( E /FinExt F /\ F /FinExt K ) ) )

Proof

Step Hyp Ref Expression
1 extdgmul 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E [:] K ) = ( ( E [:] F ) *e ( F [:] K ) ) )
2 1 eleq1d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( ( E [:] K ) e. NN0 <-> ( ( E [:] F ) *e ( F [:] K ) ) e. NN0 ) )
3 fldexttr 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> E /FldExt K )
4 brfinext 
 |-  ( E /FldExt K -> ( E /FinExt K <-> ( E [:] K ) e. NN0 ) )
5 3 4 syl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E /FinExt K <-> ( E [:] K ) e. NN0 ) )
6 brfinext 
 |-  ( E /FldExt F -> ( E /FinExt F <-> ( E [:] F ) e. NN0 ) )
7 brfinext 
 |-  ( F /FldExt K -> ( F /FinExt K <-> ( F [:] K ) e. NN0 ) )
8 6 7 bi2anan9 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( ( E /FinExt F /\ F /FinExt K ) <-> ( ( E [:] F ) e. NN0 /\ ( F [:] K ) e. NN0 ) ) )
9 extdgcl 
 |-  ( E /FldExt F -> ( E [:] F ) e. NN0* )
10 9 adantr 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E [:] F ) e. NN0* )
11 extdgcl 
 |-  ( F /FldExt K -> ( F [:] K ) e. NN0* )
12 11 adantl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( F [:] K ) e. NN0* )
13 extdggt0 
 |-  ( E /FldExt F -> 0 < ( E [:] F ) )
14 13 adantr 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> 0 < ( E [:] F ) )
15 14 gt0ne0d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E [:] F ) =/= 0 )
16 extdggt0 
 |-  ( F /FldExt K -> 0 < ( F [:] K ) )
17 16 adantl 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> 0 < ( F [:] K ) )
18 17 gt0ne0d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( F [:] K ) =/= 0 )
19 nn0xmulclb 
 |-  ( ( ( ( E [:] F ) e. NN0* /\ ( F [:] K ) e. NN0* ) /\ ( ( E [:] F ) =/= 0 /\ ( F [:] K ) =/= 0 ) ) -> ( ( ( E [:] F ) *e ( F [:] K ) ) e. NN0 <-> ( ( E [:] F ) e. NN0 /\ ( F [:] K ) e. NN0 ) ) )
20 10 12 15 18 19 syl22anc 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( ( ( E [:] F ) *e ( F [:] K ) ) e. NN0 <-> ( ( E [:] F ) e. NN0 /\ ( F [:] K ) e. NN0 ) ) )
21 8 20 bitr4d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( ( E /FinExt F /\ F /FinExt K ) <-> ( ( E [:] F ) *e ( F [:] K ) ) e. NN0 ) )
22 2 5 21 3bitr4d 
 |-  ( ( E /FldExt F /\ F /FldExt K ) -> ( E /FinExt K <-> ( E /FinExt F /\ F /FinExt K ) ) )