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

Metamath Proof Explorer

Theorem mhpvarcl

Description: A power series variable is a polynomial of degree 1. (Contributed by SN, 25-May-2024)

Ref Expression
Hypotheses mhpvarcl.h 
|- H = ( I mHomP R )
mhpvarcl.v 
|- V = ( I mVar R )
mhpvarcl.i 
|- ( ph -> I e. W )
mhpvarcl.r 
|- ( ph -> R e. Ring )
mhpvarcl.x 
|- ( ph -> X e. I )
Assertion mhpvarcl 
|- ( ph -> ( V ` X ) e. ( H ` 1 ) )

Proof

Step Hyp Ref Expression
1 mhpvarcl.h 
 |-  H = ( I mHomP R )
2 mhpvarcl.v 
 |-  V = ( I mVar R )
3 mhpvarcl.i 
 |-  ( ph -> I e. W )
4 mhpvarcl.r 
 |-  ( ph -> R e. Ring )
5 mhpvarcl.x 
 |-  ( ph -> X e. I )
6 iffalse 
 |-  ( -. d = ( y e. I |-> if ( y = X , 1 , 0 ) ) -> if ( d = ( y e. I |-> if ( y = X , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) )
7 eqid 
 |-  { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } = { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin }
8 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
9 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
10 3 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> I e. W )
11 4 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> R e. Ring )
12 5 adantr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> X e. I )
13 simpr 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } )
14 2 7 8 9 10 11 12 13 mvrval2 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( V ` X ) ` d ) = if ( d = ( y e. I |-> if ( y = X , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) )
15 14 eqeq1d 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( V ` X ) ` d ) = ( 0g ` R ) <-> if ( d = ( y e. I |-> if ( y = X , 1 , 0 ) ) , ( 1r ` R ) , ( 0g ` R ) ) = ( 0g ` R ) ) )
16 6 15 imbitrrid 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( -. d = ( y e. I |-> if ( y = X , 1 , 0 ) ) -> ( ( V ` X ) ` d ) = ( 0g ` R ) ) )
17 16 necon1ad 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( V ` X ) ` d ) =/= ( 0g ` R ) -> d = ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
18 nn0subm 
 |-  NN0 e. ( SubMnd ` CCfld )
19 eqid 
 |-  ( CCfld |`s NN0 ) = ( CCfld |`s NN0 )
20 cnfld0 
 |-  0 = ( 0g ` CCfld )
21 19 20 subm0 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> 0 = ( 0g ` ( CCfld |`s NN0 ) ) )
22 18 21 ax-mp 
 |-  0 = ( 0g ` ( CCfld |`s NN0 ) )
23 19 submmnd 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> ( CCfld |`s NN0 ) e. Mnd )
24 18 23 mp1i 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( CCfld |`s NN0 ) e. Mnd )
25 eqid 
 |-  ( y e. I |-> if ( y = X , 1 , 0 ) ) = ( y e. I |-> if ( y = X , 1 , 0 ) )
26 1nn0 
 |-  1 e. NN0
27 19 submbas 
 |-  ( NN0 e. ( SubMnd ` CCfld ) -> NN0 = ( Base ` ( CCfld |`s NN0 ) ) )
28 18 27 ax-mp 
 |-  NN0 = ( Base ` ( CCfld |`s NN0 ) )
29 26 28 eleqtri 
 |-  1 e. ( Base ` ( CCfld |`s NN0 ) )
30 29 a1i 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> 1 e. ( Base ` ( CCfld |`s NN0 ) ) )
31 22 24 10 12 25 30 gsummptif1n0 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( CCfld |`s NN0 ) gsum ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = 1 )
32 oveq2 
 |-  ( d = ( y e. I |-> if ( y = X , 1 , 0 ) ) -> ( ( CCfld |`s NN0 ) gsum d ) = ( ( CCfld |`s NN0 ) gsum ( y e. I |-> if ( y = X , 1 , 0 ) ) ) )
33 32 eqeq1d 
 |-  ( d = ( y e. I |-> if ( y = X , 1 , 0 ) ) -> ( ( ( CCfld |`s NN0 ) gsum d ) = 1 <-> ( ( CCfld |`s NN0 ) gsum ( y e. I |-> if ( y = X , 1 , 0 ) ) ) = 1 ) )
34 31 33 syl5ibrcom 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( d = ( y e. I |-> if ( y = X , 1 , 0 ) ) -> ( ( CCfld |`s NN0 ) gsum d ) = 1 ) )
35 17 34 syld 
 |-  ( ( ph /\ d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ) -> ( ( ( V ` X ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = 1 ) )
36 35 ralrimiva 
 |-  ( ph -> A. d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( ( V ` X ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = 1 ) )
37 eqid 
 |-  ( I mPoly R ) = ( I mPoly R )
38 eqid 
 |-  ( Base ` ( I mPoly R ) ) = ( Base ` ( I mPoly R ) )
39 26 a1i 
 |-  ( ph -> 1 e. NN0 )
40 37 2 38 3 4 5 mvrcl 
 |-  ( ph -> ( V ` X ) e. ( Base ` ( I mPoly R ) ) )
41 1 37 38 8 7 39 40 ismhp3 
 |-  ( ph -> ( ( V ` X ) e. ( H ` 1 ) <-> A. d e. { h e. ( NN0 ^m I ) | ( `' h " NN ) e. Fin } ( ( ( V ` X ) ` d ) =/= ( 0g ` R ) -> ( ( CCfld |`s NN0 ) gsum d ) = 1 ) ) )
42 36 41 mpbird 
 |-  ( ph -> ( V ` X ) e. ( H ` 1 ) )