selvply1rhmlem2

Description: Lemma for selvply1rhm : Image of the ring unit by the mapping H (Contributed by Thierry Arnoux, 4-May-2026)

	Ref	Expression
Hypotheses	selvply1rhm.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
	selvply1rhm.2	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	selvply1rhm.3	⊢ 𝑈 = ( ( 𝐼 ∖ { 𝑋 } ) mPoly 𝑅 )
	selvply1rhm.4	⊢ 𝑄 = ( Poly₁ ‘ 𝑈 )
	selvply1rhm.5	⊢ 𝐻 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
	selvply1rhm.6	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	selvply1rhm.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	selvply1rhm.8	⊢ ( 𝜑 → 𝑅 ∈ CRing )
Assertion	selvply1rhmlem2	⊢ ( 𝜑 → ( 𝐻 ‘ ( 1_r ‘ 𝑃 ) ) = ( 1_r ‘ 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		selvply1rhm.1	⊢ 𝐵 = ( Base ‘ 𝑃 )
2		selvply1rhm.2	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		selvply1rhm.3	⊢ 𝑈 = ( ( 𝐼 ∖ { 𝑋 } ) mPoly 𝑅 )
4		selvply1rhm.4	⊢ 𝑄 = ( Poly₁ ‘ 𝑈 )
5		selvply1rhm.5	⊢ 𝐻 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
6		selvply1rhm.6	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7		selvply1rhm.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
8		selvply1rhm.8	⊢ ( 𝜑 → 𝑅 ∈ CRing )
9		fveq2	⊢ ( 𝑓 = ( 1_r ‘ 𝑃 ) → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) = ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 1_r ‘ 𝑃 ) ) )
10	9	fveq1d	⊢ ( 𝑓 = ( 1_r ‘ 𝑃 ) → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 1_r ‘ 𝑃 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
11	10	mpteq2dv	⊢ ( 𝑓 = ( 1_r ‘ 𝑃 ) → ( 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 1_r ‘ 𝑃 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
12		eqid	⊢ ( algSc ‘ 𝑃 ) = ( algSc ‘ 𝑃 )
13		eqid	⊢ ( 1_r ‘ 𝑅 ) = ( 1_r ‘ 𝑅 )
14		eqid	⊢ ( 1_r ‘ 𝑃 ) = ( 1_r ‘ 𝑃 )
15	8	crngringd	⊢ ( 𝜑 → 𝑅 ∈ Ring )
16	2 12 13 14 6 15	mplascl1	⊢ ( 𝜑 → ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) = ( 1_r ‘ 𝑃 ) )
17	16	fveq2d	⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) ) = ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 1_r ‘ 𝑃 ) ) )
18		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
19		eqid	⊢ ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) = ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) )
20	18 13 15	ringidcld	⊢ ( 𝜑 → ( 1_r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
21		eqid	⊢ ( { 𝑋 } mPoly 𝑈 ) = ( { 𝑋 } mPoly 𝑈 )
22		eqid	⊢ ( ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) ∘ ( algSc ‘ 𝑈 ) ) = ( ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) ∘ ( algSc ‘ 𝑈 ) )
23	7	snssd	⊢ ( 𝜑 → { 𝑋 } ⊆ 𝐼 )
24	18 2 12 19 6 20 3 21 22 8 23	selvascl	⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( ( algSc ‘ 𝑃 ) ‘ ( 1_r ‘ 𝑅 ) ) ) = ( ( ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) ∘ ( algSc ‘ 𝑈 ) ) ‘ ( 1_r ‘ 𝑅 ) ) )
25	17 24	eqtr3d	⊢ ( 𝜑 → ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 1_r ‘ 𝑃 ) ) = ( ( ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) ∘ ( algSc ‘ 𝑈 ) ) ‘ ( 1_r ‘ 𝑅 ) ) )
26	25	fveq1d	⊢ ( 𝜑 → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 1_r ‘ 𝑃 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) ∘ ( algSc ‘ 𝑈 ) ) ‘ ( 1_r ‘ 𝑅 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
27	26	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 1_r ‘ 𝑃 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = ( ( ( ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) ∘ ( algSc ‘ 𝑈 ) ) ‘ ( 1_r ‘ 𝑅 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) )
28		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
29		eqid	⊢ ( algSc ‘ 𝑈 ) = ( algSc ‘ 𝑈 )
30	6	difexd	⊢ ( 𝜑 → ( 𝐼 ∖ { 𝑋 } ) ∈ V )
31	3 28 18 29 30 15	mplasclf	⊢ ( 𝜑 → ( algSc ‘ 𝑈 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑈 ) )
32	31 20	fvco3d	⊢ ( 𝜑 → ( ( ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) ∘ ( algSc ‘ 𝑈 ) ) ‘ ( 1_r ‘ 𝑅 ) ) = ( ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) ‘ ( ( algSc ‘ 𝑈 ) ‘ ( 1_r ‘ 𝑅 ) ) ) )
33		eqid	⊢ { ℎ ∈ ( ℕ₀ ↑_m { 𝑋 } ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } = { ℎ ∈ ( ℕ₀ ↑_m { 𝑋 } ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
34		eqid	⊢ ( 0_g ‘ 𝑈 ) = ( 0_g ‘ 𝑈 )
35		snex	⊢ { 𝑋 } ∈ V
36	35	a1i	⊢ ( 𝜑 → { 𝑋 } ∈ V )
37	3 30 15	mplringd	⊢ ( 𝜑 → 𝑈 ∈ Ring )
38	31 20	ffvelcdmd	⊢ ( 𝜑 → ( ( algSc ‘ 𝑈 ) ‘ ( 1_r ‘ 𝑅 ) ) ∈ ( Base ‘ 𝑈 ) )
39	21 33 34 28 19 36 37 38	mplascl	⊢ ( 𝜑 → ( ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) ‘ ( ( algSc ‘ 𝑈 ) ‘ ( 1_r ‘ 𝑅 ) ) ) = ( 𝑝 ∈ { ℎ ∈ ( ℕ₀ ↑_m { 𝑋 } ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑝 = ( { 𝑋 } × { 0 } ) , ( ( algSc ‘ 𝑈 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( 0_g ‘ 𝑈 ) ) ) )
40	32 39	eqtrd	⊢ ( 𝜑 → ( ( ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) ∘ ( algSc ‘ 𝑈 ) ) ‘ ( 1_r ‘ 𝑅 ) ) = ( 𝑝 ∈ { ℎ ∈ ( ℕ₀ ↑_m { 𝑋 } ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑝 = ( { 𝑋 } × { 0 } ) , ( ( algSc ‘ 𝑈 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( 0_g ‘ 𝑈 ) ) ) )
41	40	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( ( ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) ∘ ( algSc ‘ 𝑈 ) ) ‘ ( 1_r ‘ 𝑅 ) ) = ( 𝑝 ∈ { ℎ ∈ ( ℕ₀ ↑_m { 𝑋 } ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } ↦ if ( 𝑝 = ( { 𝑋 } × { 0 } ) , ( ( algSc ‘ 𝑈 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( 0_g ‘ 𝑈 ) ) ) )
42		eqeq1	⊢ ( 𝑝 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } → ( 𝑝 = ( { 𝑋 } × { 0 } ) ↔ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = ( { 𝑋 } × { 0 } ) ) )
43	42	adantl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑝 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) → ( 𝑝 = ( { 𝑋 } × { 0 } ) ↔ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = ( { 𝑋 } × { 0 } ) ) )
44		c0ex	⊢ 0 ∈ V
45	44	a1i	⊢ ( 𝜑 → 0 ∈ V )
46		xpsng	⊢ ( ( 𝑋 ∈ 𝐼 ∧ 0 ∈ V ) → ( { 𝑋 } × { 0 } ) = { ⟨ 𝑋 , 0 ⟩ } )
47	7 45 46	syl2anc	⊢ ( 𝜑 → ( { 𝑋 } × { 0 } ) = { ⟨ 𝑋 , 0 ⟩ } )
48	47	eqeq2d	⊢ ( 𝜑 → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = ( { 𝑋 } × { 0 } ) ↔ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , 0 ⟩ } ) )
49	48	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑝 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = ( { 𝑋 } × { 0 } ) ↔ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , 0 ⟩ } ) )
50		opex	⊢ ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ ∈ V
51		sneqbg	⊢ ( ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ ∈ V → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , 0 ⟩ } ↔ ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , 0 ⟩ ) )
52	50 51	mp1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , 0 ⟩ } ↔ ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , 0 ⟩ ) )
53		eqidd	⊢ ( 𝜑 → 𝑋 = 𝑋 )
54		fvexd	⊢ ( 𝜑 → ( 𝑛 ‘ ∅ ) ∈ V )
55		opthg	⊢ ( ( 𝑋 ∈ 𝐼 ∧ ( 𝑛 ‘ ∅ ) ∈ V ) → ( ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , 0 ⟩ ↔ ( 𝑋 = 𝑋 ∧ ( 𝑛 ‘ ∅ ) = 0 ) ) )
56	7 54 55	syl2anc	⊢ ( 𝜑 → ( ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , 0 ⟩ ↔ ( 𝑋 = 𝑋 ∧ ( 𝑛 ‘ ∅ ) = 0 ) ) )
57	53 56	mpbirand	⊢ ( 𝜑 → ( ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , 0 ⟩ ↔ ( 𝑛 ‘ ∅ ) = 0 ) )
58	57	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ = ⟨ 𝑋 , 0 ⟩ ↔ ( 𝑛 ‘ ∅ ) = 0 ) )
59		1oex	⊢ 1_o ∈ V
60	59	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → 1_o ∈ V )
61		nn0ex	⊢ ℕ₀ ∈ V
62	61	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → ℕ₀ ∈ V )
63		simpr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) )
64	60 62 63	elmaprd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → 𝑛 : 1_o ⟶ ℕ₀ )
65	64	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ ( 𝑛 ‘ ∅ ) = 0 ) → 𝑛 : 1_o ⟶ ℕ₀ )
66	65	feqmptd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ ( 𝑛 ‘ ∅ ) = 0 ) → 𝑛 = ( 𝑢 ∈ 1_o ↦ ( 𝑛 ‘ 𝑢 ) ) )
67		el1o	⊢ ( 𝑢 ∈ 1_o ↔ 𝑢 = ∅ )
68	67	biimpi	⊢ ( 𝑢 ∈ 1_o → 𝑢 = ∅ )
69	68	adantl	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ ( 𝑛 ‘ ∅ ) = 0 ) ∧ 𝑢 ∈ 1_o ) → 𝑢 = ∅ )
70	69	fveq2d	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ ( 𝑛 ‘ ∅ ) = 0 ) ∧ 𝑢 ∈ 1_o ) → ( 𝑛 ‘ 𝑢 ) = ( 𝑛 ‘ ∅ ) )
71		simplr	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ ( 𝑛 ‘ ∅ ) = 0 ) ∧ 𝑢 ∈ 1_o ) → ( 𝑛 ‘ ∅ ) = 0 )
72	70 71	eqtrd	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ ( 𝑛 ‘ ∅ ) = 0 ) ∧ 𝑢 ∈ 1_o ) → ( 𝑛 ‘ 𝑢 ) = 0 )
73	72	mpteq2dva	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ ( 𝑛 ‘ ∅ ) = 0 ) → ( 𝑢 ∈ 1_o ↦ ( 𝑛 ‘ 𝑢 ) ) = ( 𝑢 ∈ 1_o ↦ 0 ) )
74	66 73	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ ( 𝑛 ‘ ∅ ) = 0 ) → 𝑛 = ( 𝑢 ∈ 1_o ↦ 0 ) )
75		fconstmpt	⊢ ( 1_o × { 0 } ) = ( 𝑢 ∈ 1_o ↦ 0 )
76	75	eqeq2i	⊢ ( 𝑛 = ( 1_o × { 0 } ) ↔ 𝑛 = ( 𝑢 ∈ 1_o ↦ 0 ) )
77	74 76	sylibr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ ( 𝑛 ‘ ∅ ) = 0 ) → 𝑛 = ( 1_o × { 0 } ) )
78	76	biimpi	⊢ ( 𝑛 = ( 1_o × { 0 } ) → 𝑛 = ( 𝑢 ∈ 1_o ↦ 0 ) )
79	78	adantl	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑛 = ( 1_o × { 0 } ) ) → 𝑛 = ( 𝑢 ∈ 1_o ↦ 0 ) )
80		eqidd	⊢ ( ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑛 = ( 1_o × { 0 } ) ) ∧ 𝑢 = ∅ ) → 0 = 0 )
81		0lt1o	⊢ ∅ ∈ 1_o
82	81	a1i	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑛 = ( 1_o × { 0 } ) ) → ∅ ∈ 1_o )
83	44	a1i	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑛 = ( 1_o × { 0 } ) ) → 0 ∈ V )
84	79 80 82 83	fvmptd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑛 = ( 1_o × { 0 } ) ) → ( 𝑛 ‘ ∅ ) = 0 )
85	77 84	impbida	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( ( 𝑛 ‘ ∅ ) = 0 ↔ 𝑛 = ( 1_o × { 0 } ) ) )
86	52 58 85	3bitrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , 0 ⟩ } ↔ 𝑛 = ( 1_o × { 0 } ) ) )
87	86	adantr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑝 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) → ( { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } = { ⟨ 𝑋 , 0 ⟩ } ↔ 𝑛 = ( 1_o × { 0 } ) ) )
88	43 49 87	3bitrd	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑝 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) → ( 𝑝 = ( { 𝑋 } × { 0 } ) ↔ 𝑛 = ( 1_o × { 0 } ) ) )
89		eqid	⊢ ( 1_r ‘ 𝑈 ) = ( 1_r ‘ 𝑈 )
90	3 29 13 89 30 15	mplascl1	⊢ ( 𝜑 → ( ( algSc ‘ 𝑈 ) ‘ ( 1_r ‘ 𝑅 ) ) = ( 1_r ‘ 𝑈 ) )
91	90	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑝 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) → ( ( algSc ‘ 𝑈 ) ‘ ( 1_r ‘ 𝑅 ) ) = ( 1_r ‘ 𝑈 ) )
92	88 91	ifbieq1d	⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) ∧ 𝑝 = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) → if ( 𝑝 = ( { 𝑋 } × { 0 } ) , ( ( algSc ‘ 𝑈 ) ‘ ( 1_r ‘ 𝑅 ) ) , ( 0_g ‘ 𝑈 ) ) = if ( 𝑛 = ( 1_o × { 0 } ) , ( 1_r ‘ 𝑈 ) , ( 0_g ‘ 𝑈 ) ) )
93		breq1	⊢ ( ℎ = { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } → ( ℎ finSupp 0 ↔ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 ) )
94	35	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → { 𝑋 } ∈ V )
95	7	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → 𝑋 ∈ 𝐼 )
96	81	a1i	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → ∅ ∈ 1_o )
97	64 96	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( 𝑛 ‘ ∅ ) ∈ ℕ₀ )
98	95 97	fsnd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } : { 𝑋 } ⟶ ℕ₀ )
99	62 94 98	elmapdd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ ( ℕ₀ ↑_m { 𝑋 } ) )
100		snopfsupp	⊢ ( ( 𝑋 ∈ 𝐼 ∧ ( 𝑛 ‘ ∅ ) ∈ V ∧ 0 ∈ V ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 )
101	7 54 45 100	syl3anc	⊢ ( 𝜑 → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 )
102	101	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } finSupp 0 )
103	93 99 102	elrabd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ { ℎ ∈ ( ℕ₀ ↑_m { 𝑋 } ) ∣ ℎ finSupp 0 } )
104		eqid	⊢ { ℎ ∈ ( ℕ₀ ↑_m { 𝑋 } ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ₀ ↑_m { 𝑋 } ) ∣ ℎ finSupp 0 }
105	104	psrbasfsupp	⊢ { ℎ ∈ ( ℕ₀ ↑_m { 𝑋 } ) ∣ ℎ finSupp 0 } = { ℎ ∈ ( ℕ₀ ↑_m { 𝑋 } ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
106	103 105	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ∈ { ℎ ∈ ( ℕ₀ ↑_m { 𝑋 } ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin } )
107	28 89 37	ringidcld	⊢ ( 𝜑 → ( 1_r ‘ 𝑈 ) ∈ ( Base ‘ 𝑈 ) )
108	37	ringgrpd	⊢ ( 𝜑 → 𝑈 ∈ Grp )
109	28 34 108	grpidcld	⊢ ( 𝜑 → ( 0_g ‘ 𝑈 ) ∈ ( Base ‘ 𝑈 ) )
110	107 109	ifcld	⊢ ( 𝜑 → if ( 𝑛 = ( 1_o × { 0 } ) , ( 1_r ‘ 𝑈 ) , ( 0_g ‘ 𝑈 ) ) ∈ ( Base ‘ 𝑈 ) )
111	110	adantr	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → if ( 𝑛 = ( 1_o × { 0 } ) , ( 1_r ‘ 𝑈 ) , ( 0_g ‘ 𝑈 ) ) ∈ ( Base ‘ 𝑈 ) )
112	41 92 106 111	fvmptd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( ( ( ( algSc ‘ ( { 𝑋 } mPoly 𝑈 ) ) ∘ ( algSc ‘ 𝑈 ) ) ‘ ( 1_r ‘ 𝑅 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = if ( 𝑛 = ( 1_o × { 0 } ) , ( 1_r ‘ 𝑈 ) , ( 0_g ‘ 𝑈 ) ) )
113	27 112	eqtrd	⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ) → ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 1_r ‘ 𝑃 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) = if ( 𝑛 = ( 1_o × { 0 } ) , ( 1_r ‘ 𝑈 ) , ( 0_g ‘ 𝑈 ) ) )
114	113	mpteq2dva	⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 1_r ‘ 𝑃 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ↦ if ( 𝑛 = ( 1_o × { 0 } ) , ( 1_r ‘ 𝑈 ) , ( 0_g ‘ 𝑈 ) ) ) )
115		eqid	⊢ ( 1_o mPoly 𝑈 ) = ( 1_o mPoly 𝑈 )
116		psr1baslem	⊢ ( ℕ₀ ↑_m 1_o ) = { ℎ ∈ ( ℕ₀ ↑_m 1_o ) ∣ ( ^◡ ℎ “ ℕ ) ∈ Fin }
117		eqid	⊢ ( algSc ‘ 𝑄 ) = ( algSc ‘ 𝑄 )
118	4 117	ply1ascl	⊢ ( algSc ‘ 𝑄 ) = ( algSc ‘ ( 1_o mPoly 𝑈 ) )
119	59	a1i	⊢ ( 𝜑 → 1_o ∈ V )
120	115 116 34 28 118 119 37 107	mplascl	⊢ ( 𝜑 → ( ( algSc ‘ 𝑄 ) ‘ ( 1_r ‘ 𝑈 ) ) = ( 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ↦ if ( 𝑛 = ( 1_o × { 0 } ) , ( 1_r ‘ 𝑈 ) , ( 0_g ‘ 𝑈 ) ) ) )
121		eqid	⊢ ( 1_r ‘ 𝑄 ) = ( 1_r ‘ 𝑄 )
122	4 117 89 121 37	ply1ascl1	⊢ ( 𝜑 → ( ( algSc ‘ 𝑄 ) ‘ ( 1_r ‘ 𝑈 ) ) = ( 1_r ‘ 𝑄 ) )
123	114 120 122	3eqtr2d	⊢ ( 𝜑 → ( 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ ( 1_r ‘ 𝑃 ) ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 1_r ‘ 𝑄 ) )
124	11 123	sylan9eqr	⊢ ( ( 𝜑 ∧ 𝑓 = ( 1_r ‘ 𝑃 ) ) → ( 𝑛 ∈ ( ℕ₀ ↑_m 1_o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) = ( 1_r ‘ 𝑄 ) )
125	2 6 15	mplringd	⊢ ( 𝜑 → 𝑃 ∈ Ring )
126	1 14 125	ringidcld	⊢ ( 𝜑 → ( 1_r ‘ 𝑃 ) ∈ 𝐵 )
127		fvexd	⊢ ( 𝜑 → ( 1_r ‘ 𝑄 ) ∈ V )
128	5 124 126 127	fvmptd2	⊢ ( 𝜑 → ( 𝐻 ‘ ( 1_r ‘ 𝑃 ) ) = ( 1_r ‘ 𝑄 ) )

Metamath Proof Explorer

Theorem selvply1rhmlem2

Proof