Theorem 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	⊢ 𝑄 = ( Poly1 ‘ 𝑈 )
	selvply1rhm.5	⊢ 𝐻 = ( 𝑓 ∈ 𝐵 ↦ ( 𝑛 ∈ ( ℕ0 ↑m 1o ) ↦ ( ( ( ( 𝐼 selectVars 𝑅 ) ‘ { 𝑋 } ) ‘ 𝑓 ) ‘ { ⟨ 𝑋 , ( 𝑛 ‘ ∅ ) ⟩ } ) ) )
	selvply1rhm.6	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	selvply1rhm.7	⊢ ( 𝜑 → 𝑋 ∈ 𝐼 )
	selvply1rhm.8	⊢ ( 𝜑 → 𝑅 ∈ CRing )
Assertion	selvply1rhmlem2	⊢ ( 𝜑 → ( 𝐻 ‘ ( 1r ‘ 𝑃 ) ) = ( 1r ‘ 𝑄 ) )

Proof

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