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

Metamath Proof Explorer

Theorem extdgfialg

Description: A finite field extension E / F is algebraic. Part of the proof of Proposition 1.1 of Lang, p. 224. (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses extdgfialg.b 
|- B = ( Base ` E )
extdgfialg.d 
|- D = ( dim ` ( ( subringAlg ` E ) ` F ) )
extdgfialg.e 
|- ( ph -> E e. Field )
extdgfialg.f 
|- ( ph -> F e. ( SubDRing ` E ) )
extdgfialg.1 
|- ( ph -> D e. NN0 )
Assertion extdgfialg 
|- ( ph -> ( E IntgRing F ) = B )

Proof

Step Hyp Ref Expression
1 extdgfialg.b 
 |-  B = ( Base ` E )
2 extdgfialg.d 
 |-  D = ( dim ` ( ( subringAlg ` E ) ` F ) )
3 extdgfialg.e 
 |-  ( ph -> E e. Field )
4 extdgfialg.f 
 |-  ( ph -> F e. ( SubDRing ` E ) )
5 extdgfialg.1 
 |-  ( ph -> D e. NN0 )
6 eqid 
 |-  ( E evalSub1 F ) = ( E evalSub1 F )
7 eqid 
 |-  ( E |`s F ) = ( E |`s F )
8 eqid 
 |-  ( 0g ` E ) = ( 0g ` E )
9 3 fldcrngd 
 |-  ( ph -> E e. CRing )
10 sdrgsubrg 
 |-  ( F e. ( SubDRing ` E ) -> F e. ( SubRing ` E ) )
11 4 10 syl 
 |-  ( ph -> F e. ( SubRing ` E ) )
12 6 7 1 8 9 11 irngssv 
 |-  ( ph -> ( E IntgRing F ) C_ B )
13 3 adantr 
 |-  ( ( ph /\ x e. B ) -> E e. Field )
14 13 ad4antr 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ a finSupp ( 0g ` E ) ) /\ ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) -> E e. Field )
15 4 adantr 
 |-  ( ( ph /\ x e. B ) -> F e. ( SubDRing ` E ) )
16 15 ad4antr 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ a finSupp ( 0g ` E ) ) /\ ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) -> F e. ( SubDRing ` E ) )
17 5 adantr 
 |-  ( ( ph /\ x e. B ) -> D e. NN0 )
18 17 ad4antr 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ a finSupp ( 0g ` E ) ) /\ ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) -> D e. NN0 )
19 eqid 
 |-  ( .r ` E ) = ( .r ` E )
20 oveq1 
 |-  ( m = n -> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) = ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) )
21 20 cbvmptv 
 |-  ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) = ( n e. ( 0 ... D ) |-> ( n ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) )
22 simpr 
 |-  ( ( ph /\ x e. B ) -> x e. B )
23 22 ad4antr 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ a finSupp ( 0g ` E ) ) /\ ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) -> x e. B )
24 ovexd 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ a finSupp ( 0g ` E ) ) /\ ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) -> ( 0 ... D ) e. _V )
25 simp-4r 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ a finSupp ( 0g ` E ) ) /\ ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) -> a e. ( F ^m ( 0 ... D ) ) )
26 24 16 25 elmaprd 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ a finSupp ( 0g ` E ) ) /\ ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) -> a : ( 0 ... D ) --> F )
27 simpllr 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ a finSupp ( 0g ` E ) ) /\ ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) -> a finSupp ( 0g ` E ) )
28 simplr 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ a finSupp ( 0g ` E ) ) /\ ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) -> ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) )
29 simpr 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ a finSupp ( 0g ` E ) ) /\ ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) -> a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) )
30 1 2 14 16 18 8 19 21 23 26 27 28 29 extdgfialglem2 
 |-  ( ( ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ a finSupp ( 0g ` E ) ) /\ ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) -> x e. ( E IntgRing F ) )
31 30 anasss 
 |-  ( ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ a finSupp ( 0g ` E ) ) /\ ( ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) ) -> x e. ( E IntgRing F ) )
32 31 anasss 
 |-  ( ( ( ( ph /\ x e. B ) /\ a e. ( F ^m ( 0 ... D ) ) ) /\ ( a finSupp ( 0g ` E ) /\ ( ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) ) ) -> x e. ( E IntgRing F ) )
33 1 2 13 15 17 8 19 21 22 extdgfialglem1 
 |-  ( ( ph /\ x e. B ) -> E. a e. ( F ^m ( 0 ... D ) ) ( a finSupp ( 0g ` E ) /\ ( ( E gsum ( a oF ( .r ` E ) ( m e. ( 0 ... D ) |-> ( m ( .g ` ( mulGrp ` ( ( subringAlg ` E ) ` F ) ) ) x ) ) ) ) = ( 0g ` E ) /\ a =/= ( ( 0 ... D ) X. { ( 0g ` E ) } ) ) ) )
34 32 33 r19.29a 
 |-  ( ( ph /\ x e. B ) -> x e. ( E IntgRing F ) )
35 12 34 eqelssd 
 |-  ( ph -> ( E IntgRing F ) = B )