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 ⊢ 𝑋 = ( var1 ‘ 𝑈 )
vr1nz.z ⊢ 𝑍 = ( 0g ‘ 𝑃 )
vr1nz.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
vr1nz.p ⊢ 𝑃 = ( Poly1 ‘ 𝑈 )
vr1nz.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
vr1nz.1 ⊢ ( 𝜑 → 𝑆 ∈ NzRing )
vr1nz.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
Assertion vr1nz ( 𝜑 → 𝑋 ≠ 𝑍 )

Proof

Step Hyp Ref Expression
1 vr1nz.x ⊢ 𝑋 = ( var1 ‘ 𝑈 )
2 vr1nz.z ⊢ 𝑍 = ( 0g ‘ 𝑃 )
3 vr1nz.u ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
4 vr1nz.p ⊢ 𝑃 = ( Poly1 ‘ 𝑈 )
5 vr1nz.s ⊢ ( 𝜑 → 𝑆 ∈ CRing )
6 vr1nz.1 ⊢ ( 𝜑 → 𝑆 ∈ NzRing )
7 vr1nz.r ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
8 eqid ⊢ ( 1r ‘ 𝑆 ) = ( 1r ‘ 𝑆 )
9 eqid ⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
10 8 9 nzrnz ⊢ ( 𝑆 ∈ NzRing → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
11 6 10 syl ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ≠ ( 0g ‘ 𝑆 ) )
12 5 crnggrpd ⊢ ( 𝜑 → 𝑆 ∈ Grp )
13 12 grpmndd ⊢ ( 𝜑 → 𝑆 ∈ Mnd )
14 subrgsubg ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ∈ ( SubGrp ‘ 𝑆 ) )
15 9 subg0cl ⊢ ( 𝑅 ∈ ( SubGrp ‘ 𝑆 ) → ( 0g ‘ 𝑆 ) ∈ 𝑅 )
16 7 14 15 3syl ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ 𝑅 )
17 eqid ⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
18 17 subrgss ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑅 ⊆ ( Base ‘ 𝑆 ) )
19 7 18 syl ⊢ ( 𝜑 → 𝑅 ⊆ ( Base ‘ 𝑆 ) )
20 3 17 9 ress0g ⊢ ( ( 𝑆 ∈ Mnd ∧ ( 0g ‘ 𝑆 ) ∈ 𝑅 ∧ 𝑅 ⊆ ( Base ‘ 𝑆 ) ) → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
21 13 16 19 20 syl3anc ⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑈 ) )
22 21 fveq2d ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) = ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) )
23 22 fveq2d ⊢ ( 𝜑 → ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) ) = ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) ) )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) ) = ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) ) )
25 3 subrgring ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
26 eqid ⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
27 eqid ⊢ ( 0g ‘ 𝑈 ) = ( 0g ‘ 𝑈 )
28 4 26 27 2 ply1scl0 ⊢ ( 𝑈 ∈ Ring → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) = 𝑍 )
29 7 25 28 3syl ⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) = 𝑍 )
30 29 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) = 𝑍 )
31 simpr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → 𝑋 = 𝑍 )
32 30 31 eqtr4d ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) = 𝑋 )
33 32 fveq2d ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑈 ) ) ) = ( ( 𝑆 evalSub1 𝑅 ) ‘ 𝑋 ) )
34 eqid ⊢ ( 𝑆 evalSub1 𝑅 ) = ( 𝑆 evalSub1 𝑅 )
35 34 1 3 17 5 7 evls1var ⊢ ( 𝜑 → ( ( 𝑆 evalSub1 𝑅 ) ‘ 𝑋 ) = ( I ↾ ( Base ‘ 𝑆 ) ) )
36 35 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( 𝑆 evalSub1 𝑅 ) ‘ 𝑋 ) = ( I ↾ ( Base ‘ 𝑆 ) ) )
37 24 33 36 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) ) = ( I ↾ ( Base ‘ 𝑆 ) ) )
38 37 fveq1d ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( ( I ↾ ( Base ‘ 𝑆 ) ) ‘ ( 1r ‘ 𝑆 ) ) )
39 5 crngringd ⊢ ( 𝜑 → 𝑆 ∈ Ring )
40 17 8 39 ringidcld ⊢ ( 𝜑 → ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) )
41 34 4 3 17 26 5 7 16 40 evls1scafv ⊢ ( 𝜑 → ( ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( 0g ‘ 𝑆 ) )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( ( 𝑆 evalSub1 𝑅 ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 0g ‘ 𝑆 ) ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( 0g ‘ 𝑆 ) )
43 fvresi ⊢ ( ( 1r ‘ 𝑆 ) ∈ ( Base ‘ 𝑆 ) → ( ( I ↾ ( Base ‘ 𝑆 ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( 1r ‘ 𝑆 ) )
44 40 43 syl ⊢ ( 𝜑 → ( ( I ↾ ( Base ‘ 𝑆 ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( 1r ‘ 𝑆 ) )
45 44 adantr ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( ( I ↾ ( Base ‘ 𝑆 ) ) ‘ ( 1r ‘ 𝑆 ) ) = ( 1r ‘ 𝑆 ) )
46 38 42 45 3eqtr3rd ⊢ ( ( 𝜑 ∧ 𝑋 = 𝑍 ) → ( 1r ‘ 𝑆 ) = ( 0g ‘ 𝑆 ) )
47 11 46 mteqand ⊢ ( 𝜑 → 𝑋 ≠ 𝑍 )