coe1z

Description: The coefficient vector of 0. (Contributed by Stefan O'Rear, 23-Mar-2015)

	Ref	Expression
Hypotheses	coe1z.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
	coe1z.z	⊢ 0 = ( 0_g ‘ 𝑃 )
	coe1z.y	⊢ 𝑌 = ( 0_g ‘ 𝑅 )
Assertion	coe1z	⊢ ( 𝑅 ∈ Ring → ( coe₁ ‘ 0 ) = ( ℕ₀ × { 𝑌 } ) )

Proof

Step	Hyp	Ref	Expression
1		coe1z.p	⊢ 𝑃 = ( Poly₁ ‘ 𝑅 )
2		coe1z.z	⊢ 0 = ( 0_g ‘ 𝑃 )
3		coe1z.y	⊢ 𝑌 = ( 0_g ‘ 𝑅 )
4		fconst6g	⊢ ( 𝑎 ∈ ℕ₀ → ( 1_o × { 𝑎 } ) : 1_o ⟶ ℕ₀ )
5	4	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ ℕ₀ ) → ( 1_o × { 𝑎 } ) : 1_o ⟶ ℕ₀ )
6		nn0ex	⊢ ℕ₀ ∈ V
7		1oex	⊢ 1_o ∈ V
8	6 7	elmap	⊢ ( ( 1_o × { 𝑎 } ) ∈ ( ℕ₀ ↑_m 1_o ) ↔ ( 1_o × { 𝑎 } ) : 1_o ⟶ ℕ₀ )
9	5 8	sylibr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑎 ∈ ℕ₀ ) → ( 1_o × { 𝑎 } ) ∈ ( ℕ₀ ↑_m 1_o ) )
10		eqidd	⊢ ( 𝑅 ∈ Ring → ( 𝑎 ∈ ℕ₀ ↦ ( 1_o × { 𝑎 } ) ) = ( 𝑎 ∈ ℕ₀ ↦ ( 1_o × { 𝑎 } ) ) )
11		eqid	⊢ ( 1_o mPoly 𝑅 ) = ( 1_o mPoly 𝑅 )
12		psr1baslem	⊢ ( ℕ₀ ↑_m 1_o ) = { 𝑐 ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ 𝑐 “ ℕ ) ∈ Fin }
13	11 1 2	ply1mpl0	⊢ 0 = ( 0_g ‘ ( 1_o mPoly 𝑅 ) )
14		1on	⊢ 1_o ∈ On
15	14	a1i	⊢ ( 𝑅 ∈ Ring → 1_o ∈ On )
16		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
17	11 12 3 13 15 16	mpl0	⊢ ( 𝑅 ∈ Ring → 0 = ( ( ℕ₀ ↑_m 1_o ) × { 𝑌 } ) )
18		fconstmpt	⊢ ( ( ℕ₀ ↑_m 1_o ) × { 𝑌 } ) = ( 𝑏 ∈ ( ℕ₀ ↑_m 1_o ) ↦ 𝑌 )
19	17 18	eqtrdi	⊢ ( 𝑅 ∈ Ring → 0 = ( 𝑏 ∈ ( ℕ₀ ↑_m 1_o ) ↦ 𝑌 ) )
20		eqidd	⊢ ( 𝑏 = ( 1_o × { 𝑎 } ) → 𝑌 = 𝑌 )
21	9 10 19 20	fmptco	⊢ ( 𝑅 ∈ Ring → ( 0 ∘ ( 𝑎 ∈ ℕ₀ ↦ ( 1_o × { 𝑎 } ) ) ) = ( 𝑎 ∈ ℕ₀ ↦ 𝑌 ) )
22	1	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
23		eqid	⊢ ( Base ‘ 𝑃 ) = ( Base ‘ 𝑃 )
24	23 2	ring0cl	⊢ ( 𝑃 ∈ Ring → 0 ∈ ( Base ‘ 𝑃 ) )
25		eqid	⊢ ( coe₁ ‘ 0 ) = ( coe₁ ‘ 0 )
26		eqid	⊢ ( 𝑎 ∈ ℕ₀ ↦ ( 1_o × { 𝑎 } ) ) = ( 𝑎 ∈ ℕ₀ ↦ ( 1_o × { 𝑎 } ) )
27	25 23 1 26	coe1fval2	⊢ ( 0 ∈ ( Base ‘ 𝑃 ) → ( coe₁ ‘ 0 ) = ( 0 ∘ ( 𝑎 ∈ ℕ₀ ↦ ( 1_o × { 𝑎 } ) ) ) )
28	22 24 27	3syl	⊢ ( 𝑅 ∈ Ring → ( coe₁ ‘ 0 ) = ( 0 ∘ ( 𝑎 ∈ ℕ₀ ↦ ( 1_o × { 𝑎 } ) ) ) )
29		fconstmpt	⊢ ( ℕ₀ × { 𝑌 } ) = ( 𝑎 ∈ ℕ₀ ↦ 𝑌 )
30	29	a1i	⊢ ( 𝑅 ∈ Ring → ( ℕ₀ × { 𝑌 } ) = ( 𝑎 ∈ ℕ₀ ↦ 𝑌 ) )
31	21 28 30	3eqtr4d	⊢ ( 𝑅 ∈ Ring → ( coe₁ ‘ 0 ) = ( ℕ₀ × { 𝑌 } ) )

Metamath Proof Explorer

Theorem coe1z

Proof