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

Metamath Proof Explorer

Theorem vr1nz

Description: A univariate polynomial variable cannot be the zero polynomial. (Contributed by Thierry Arnoux, 14-Nov-2025)

Ref Expression
Hypotheses vr1nz.x 
|- X = ( var1 ` U )
vr1nz.z 
|- Z = ( 0g ` P )
vr1nz.u 
|- U = ( S |`s R )
vr1nz.p 
|- P = ( Poly1 ` U )
vr1nz.s 
|- ( ph -> S e. CRing )
vr1nz.1 
|- ( ph -> S e. NzRing )
vr1nz.r 
|- ( ph -> R e. ( SubRing ` S ) )
Assertion vr1nz 
|- ( ph -> X =/= Z )

Proof

Step Hyp Ref Expression
1 vr1nz.x 
 |-  X = ( var1 ` U )
2 vr1nz.z 
 |-  Z = ( 0g ` P )
3 vr1nz.u 
 |-  U = ( S |`s R )
4 vr1nz.p 
 |-  P = ( Poly1 ` U )
5 vr1nz.s 
 |-  ( ph -> S e. CRing )
6 vr1nz.1 
 |-  ( ph -> S e. NzRing )
7 vr1nz.r 
 |-  ( ph -> R e. ( SubRing ` S ) )
8 eqid 
 |-  ( 1r ` S ) = ( 1r ` S )
9 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
10 8 9 nzrnz 
 |-  ( S e. NzRing -> ( 1r ` S ) =/= ( 0g ` S ) )
11 6 10 syl 
 |-  ( ph -> ( 1r ` S ) =/= ( 0g ` S ) )
12 5 crnggrpd 
 |-  ( ph -> S e. Grp )
13 12 grpmndd 
 |-  ( ph -> S e. Mnd )
14 subrgsubg 
 |-  ( R e. ( SubRing ` S ) -> R e. ( SubGrp ` S ) )
15 9 subg0cl 
 |-  ( R e. ( SubGrp ` S ) -> ( 0g ` S ) e. R )
16 7 14 15 3syl 
 |-  ( ph -> ( 0g ` S ) e. R )
17 eqid 
 |-  ( Base ` S ) = ( Base ` S )
18 17 subrgss 
 |-  ( R e. ( SubRing ` S ) -> R C_ ( Base ` S ) )
19 7 18 syl 
 |-  ( ph -> R C_ ( Base ` S ) )
20 3 17 9 ress0g 
 |-  ( ( S e. Mnd /\ ( 0g ` S ) e. R /\ R C_ ( Base ` S ) ) -> ( 0g ` S ) = ( 0g ` U ) )
21 13 16 19 20 syl3anc 
 |-  ( ph -> ( 0g ` S ) = ( 0g ` U ) )
22 21 fveq2d 
 |-  ( ph -> ( ( algSc ` P ) ` ( 0g ` S ) ) = ( ( algSc ` P ) ` ( 0g ` U ) ) )
23 22 fveq2d 
 |-  ( ph -> ( ( S evalSub1 R ) ` ( ( algSc ` P ) ` ( 0g ` S ) ) ) = ( ( S evalSub1 R ) ` ( ( algSc ` P ) ` ( 0g ` U ) ) ) )
24 23 adantr 
 |-  ( ( ph /\ X = Z ) -> ( ( S evalSub1 R ) ` ( ( algSc ` P ) ` ( 0g ` S ) ) ) = ( ( S evalSub1 R ) ` ( ( algSc ` P ) ` ( 0g ` U ) ) ) )
25 3 subrgring 
 |-  ( R e. ( SubRing ` S ) -> U e. Ring )
26 eqid 
 |-  ( algSc ` P ) = ( algSc ` P )
27 eqid 
 |-  ( 0g ` U ) = ( 0g ` U )
28 4 26 27 2 ply1scl0 
 |-  ( U e. Ring -> ( ( algSc ` P ) ` ( 0g ` U ) ) = Z )
29 7 25 28 3syl 
 |-  ( ph -> ( ( algSc ` P ) ` ( 0g ` U ) ) = Z )
30 29 adantr 
 |-  ( ( ph /\ X = Z ) -> ( ( algSc ` P ) ` ( 0g ` U ) ) = Z )
31 simpr 
 |-  ( ( ph /\ X = Z ) -> X = Z )
32 30 31 eqtr4d 
 |-  ( ( ph /\ X = Z ) -> ( ( algSc ` P ) ` ( 0g ` U ) ) = X )
33 32 fveq2d 
 |-  ( ( ph /\ X = Z ) -> ( ( S evalSub1 R ) ` ( ( algSc ` P ) ` ( 0g ` U ) ) ) = ( ( S evalSub1 R ) ` X ) )
34 eqid 
 |-  ( S evalSub1 R ) = ( S evalSub1 R )
35 34 1 3 17 5 7 evls1var 
 |-  ( ph -> ( ( S evalSub1 R ) ` X ) = ( _I |` ( Base ` S ) ) )
36 35 adantr 
 |-  ( ( ph /\ X = Z ) -> ( ( S evalSub1 R ) ` X ) = ( _I |` ( Base ` S ) ) )
37 24 33 36 3eqtrd 
 |-  ( ( ph /\ X = Z ) -> ( ( S evalSub1 R ) ` ( ( algSc ` P ) ` ( 0g ` S ) ) ) = ( _I |` ( Base ` S ) ) )
38 37 fveq1d 
 |-  ( ( ph /\ X = Z ) -> ( ( ( S evalSub1 R ) ` ( ( algSc ` P ) ` ( 0g ` S ) ) ) ` ( 1r ` S ) ) = ( ( _I |` ( Base ` S ) ) ` ( 1r ` S ) ) )
39 5 crngringd 
 |-  ( ph -> S e. Ring )
40 17 8 39 ringidcld 
 |-  ( ph -> ( 1r ` S ) e. ( Base ` S ) )
41 34 4 3 17 26 5 7 16 40 evls1scafv 
 |-  ( ph -> ( ( ( S evalSub1 R ) ` ( ( algSc ` P ) ` ( 0g ` S ) ) ) ` ( 1r ` S ) ) = ( 0g ` S ) )
42 41 adantr 
 |-  ( ( ph /\ X = Z ) -> ( ( ( S evalSub1 R ) ` ( ( algSc ` P ) ` ( 0g ` S ) ) ) ` ( 1r ` S ) ) = ( 0g ` S ) )
43 fvresi 
 |-  ( ( 1r ` S ) e. ( Base ` S ) -> ( ( _I |` ( Base ` S ) ) ` ( 1r ` S ) ) = ( 1r ` S ) )
44 40 43 syl 
 |-  ( ph -> ( ( _I |` ( Base ` S ) ) ` ( 1r ` S ) ) = ( 1r ` S ) )
45 44 adantr 
 |-  ( ( ph /\ X = Z ) -> ( ( _I |` ( Base ` S ) ) ` ( 1r ` S ) ) = ( 1r ` S ) )
46 38 42 45 3eqtr3rd 
 |-  ( ( ph /\ X = Z ) -> ( 1r ` S ) = ( 0g ` S ) )
47 11 46 mteqand 
 |-  ( ph -> X =/= Z )