Metamath Proof Explorer

Theorem evls1monply1

Description: Subring evaluation of a scaled monomial. (Contributed by Thierry Arnoux, 10-Jan-2026)

Ref Expression
Hypotheses evls1monply1.1 ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
evls1monply1.2 ⊢ 𝐾 = ( Base ‘ 𝑆 )
evls1monply1.3 ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
evls1monply1.4 ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
evls1monply1.5 ⊢ 𝑋 = ( var1 ‘ 𝑈 )
evls1monply1.6 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
evls1monply1.7 ⊢ ∧ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
evls1monply1.8 ⊢ ∗ = ( ·𝑠 ‘ 𝑊 )
evls1monply1.9 ⊢ · = ( .r ‘ 𝑆 )
evls1monply1.10 ⊢ ( 𝜑 → 𝑆 ∈ CRing )
evls1monply1.11 ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
evls1monply1.12 ⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
evls1monply1.13 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
evls1monply1.14 ⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
Assertion evls1monply1 ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ∗ ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝑌 ) = ( 𝐴 · ( 𝑁 ∧ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 evls1monply1.1 ⊢ 𝑄 = ( 𝑆 evalSub1 𝑅 )
2 evls1monply1.2 ⊢ 𝐾 = ( Base ‘ 𝑆 )
3 evls1monply1.3 ⊢ 𝑊 = ( Poly1 ‘ 𝑈 )
4 evls1monply1.4 ⊢ 𝑈 = ( 𝑆 ↾s 𝑅 )
5 evls1monply1.5 ⊢ 𝑋 = ( var1 ‘ 𝑈 )
6 evls1monply1.6 ⊢ ↑ = ( .g ‘ ( mulGrp ‘ 𝑊 ) )
7 evls1monply1.7 ⊢ ∧ = ( .g ‘ ( mulGrp ‘ 𝑆 ) )
8 evls1monply1.8 ⊢ ∗ = ( ·𝑠 ‘ 𝑊 )
9 evls1monply1.9 ⊢ · = ( .r ‘ 𝑆 )
10 evls1monply1.10 ⊢ ( 𝜑 → 𝑆 ∈ CRing )
11 evls1monply1.11 ⊢ ( 𝜑 → 𝑅 ∈ ( SubRing ‘ 𝑆 ) )
12 evls1monply1.12 ⊢ ( 𝜑 → 𝐴 ∈ 𝑅 )
13 evls1monply1.13 ⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
14 evls1monply1.14 ⊢ ( 𝜑 → 𝑌 ∈ 𝐾 )
15 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
16 eqid ⊢ ( mulGrp ‘ 𝑊 ) = ( mulGrp ‘ 𝑊 )
17 16 15 mgpbas ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ ( mulGrp ‘ 𝑊 ) )
18 4 subrgring ⊢ ( 𝑅 ∈ ( SubRing ‘ 𝑆 ) → 𝑈 ∈ Ring )
19 11 18 syl ⊢ ( 𝜑 → 𝑈 ∈ Ring )
20 3 ply1ring ⊢ ( 𝑈 ∈ Ring → 𝑊 ∈ Ring )
21 16 ringmgp ⊢ ( 𝑊 ∈ Ring → ( mulGrp ‘ 𝑊 ) ∈ Mnd )
22 19 20 21 3syl ⊢ ( 𝜑 → ( mulGrp ‘ 𝑊 ) ∈ Mnd )
23 5 3 15 vr1cl ⊢ ( 𝑈 ∈ Ring → 𝑋 ∈ ( Base ‘ 𝑊 ) )
24 19 23 syl ⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑊 ) )
25 17 6 22 13 24 mulgnn0cld ⊢ ( 𝜑 → ( 𝑁 ↑ 𝑋 ) ∈ ( Base ‘ 𝑊 ) )
26 1 2 3 4 15 8 9 10 11 12 25 14 evls1vsca ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ∗ ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝑌 ) = ( 𝐴 · ( ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝑌 ) ) )
27 1 4 3 5 2 6 7 10 11 13 14 evls1varpwval ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝑌 ) = ( 𝑁 ∧ 𝑌 ) )
28 27 oveq2d ⊢ ( 𝜑 → ( 𝐴 · ( ( 𝑄 ‘ ( 𝑁 ↑ 𝑋 ) ) ‘ 𝑌 ) ) = ( 𝐴 · ( 𝑁 ∧ 𝑌 ) ) )
29 26 28 eqtrd ⊢ ( 𝜑 → ( ( 𝑄 ‘ ( 𝐴 ∗ ( 𝑁 ↑ 𝑋 ) ) ) ‘ 𝑌 ) = ( 𝐴 · ( 𝑁 ∧ 𝑌 ) ) )