Theorem selvval2lem4

Description: The fourth argument passed to evalSub is in the domain (a polynomial in ( I mPoly ( J mPoly ( ( I \ J ) mPoly R ) ) ) ). (Contributed by SN, 5-Nov-2023)

	Ref	Expression
Hypotheses	selvval2lem4.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	selvval2lem4.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
	selvval2lem4.u	⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
	selvval2lem4.t	⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
	selvval2lem4.c	⊢ 𝐶 = ( algSc ‘ 𝑇 )
	selvval2lem4.d	⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
	selvval2lem4.s	⊢ 𝑆 = ( 𝑇 ↾s ran 𝐷 )
	selvval2lem4.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑆 )
	selvval2lem4.x	⊢ 𝑋 = ( Base ‘ 𝑊 )
	selvval2lem4.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	selvval2lem4.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	selvval2lem4.j	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
	selvval2lem4.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	selvval2lem4	⊢ ( 𝜑 → ( 𝐷 ∘ 𝐹 ) ∈ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		selvval2lem4.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
2		selvval2lem4.b	⊢ 𝐵 = ( Base ‘ 𝑃 )
3		selvval2lem4.u	⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
4		selvval2lem4.t	⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
5		selvval2lem4.c	⊢ 𝐶 = ( algSc ‘ 𝑇 )
6		selvval2lem4.d	⊢ 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) )
7		selvval2lem4.s	⊢ 𝑆 = ( 𝑇 ↾s ran 𝐷 )
8		selvval2lem4.w	⊢ 𝑊 = ( 𝐼 mPoly 𝑆 )
9		selvval2lem4.x	⊢ 𝑋 = ( Base ‘ 𝑊 )
10		selvval2lem4.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
11		selvval2lem4.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
12		selvval2lem4.j	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
13		selvval2lem4.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
14	10	difexd	⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
15	10 12	ssexd	⊢ ( 𝜑 → 𝐽 ∈ V )
16	3 4 5 6 14 15 11	selvval2lem2	⊢ ( 𝜑 → 𝐷 ∈ ( 𝑅 RingHom 𝑇 ) )
17		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
18		eqid	⊢ ( Base ‘ 𝑇 ) = ( Base ‘ 𝑇 )
19	17 18	rhmf	⊢ ( 𝐷 ∈ ( 𝑅 RingHom 𝑇 ) → 𝐷 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑇 ) )
20		ffrn	⊢ ( 𝐷 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑇 ) → 𝐷 : ( Base ‘ 𝑅 ) ⟶ ran 𝐷 )
21	16 19 20	3syl	⊢ ( 𝜑 → 𝐷 : ( Base ‘ 𝑅 ) ⟶ ran 𝐷 )
22	3 4 5 6 14 15 11	selvval2lem3	⊢ ( 𝜑 → ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) )
23	18	subrgss	⊢ ( ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) → ran 𝐷 ⊆ ( Base ‘ 𝑇 ) )
24	7 18	ressbas2	⊢ ( ran 𝐷 ⊆ ( Base ‘ 𝑇 ) → ran 𝐷 = ( Base ‘ 𝑆 ) )
25	22 23 24	3syl	⊢ ( 𝜑 → ran 𝐷 = ( Base ‘ 𝑆 ) )
26	25	feq3d	⊢ ( 𝜑 → ( 𝐷 : ( Base ‘ 𝑅 ) ⟶ ran 𝐷 ↔ 𝐷 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) ) )
27	21 26	mpbid	⊢ ( 𝜑 → 𝐷 : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑆 ) )
28		eqid	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
29	1 17 2 28 13	mplelf	⊢ ( 𝜑 → 𝐹 : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑅 ) )
30	27 29	fcod	⊢ ( 𝜑 → ( 𝐷 ∘ 𝐹 ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑆 ) )
31		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑆 ) ∈ V )
32		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
33	32	rabex	⊢ { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V
34	33	a1i	⊢ ( 𝜑 → { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ∈ V )
35	31 34	elmapd	⊢ ( 𝜑 → ( ( 𝐷 ∘ 𝐹 ) ∈ ( ( Base ‘ 𝑆 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) ↔ ( 𝐷 ∘ 𝐹 ) : { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ⟶ ( Base ‘ 𝑆 ) ) )
36	30 35	mpbird	⊢ ( 𝜑 → ( 𝐷 ∘ 𝐹 ) ∈ ( ( Base ‘ 𝑆 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
37		eqid	⊢ ( 𝐼 mPwSer 𝑆 ) = ( 𝐼 mPwSer 𝑆 )
38		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
39		eqid	⊢ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) = ( Base ‘ ( 𝐼 mPwSer 𝑆 ) )
40	37 38 28 39 10	psrbas	⊢ ( 𝜑 → ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) = ( ( Base ‘ 𝑆 ) ↑m { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin } ) )
41	36 40	eleqtrrd	⊢ ( 𝜑 → ( 𝐷 ∘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) )
42		fvexd	⊢ ( 𝜑 → ( 0g ‘ 𝑆 ) ∈ V )
43		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
44		eqid	⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
45	17 44	ring0cl	⊢ ( 𝑅 ∈ Ring → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
46	11 43 45	3syl	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
47		ssidd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ⊆ ( Base ‘ 𝑅 ) )
48		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑅 ) ∈ V )
49	1 2 44 13 11	mplelsfi	⊢ ( 𝜑 → 𝐹 finSupp ( 0g ‘ 𝑅 ) )
50	6	a1i	⊢ ( 𝜑 → 𝐷 = ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) )
51	50	fveq1d	⊢ ( 𝜑 → ( 𝐷 ‘ ( 0g ‘ 𝑅 ) ) = ( ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) ‘ ( 0g ‘ 𝑅 ) ) )
52		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
53		eqid	⊢ ( algSc ‘ 𝑈 ) = ( algSc ‘ 𝑈 )
54	11 43	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
55	3 52 17 53 14 54	mplasclf	⊢ ( 𝜑 → ( algSc ‘ 𝑈 ) : ( Base ‘ 𝑅 ) ⟶ ( Base ‘ 𝑈 ) )
56	55 46	fvco3d	⊢ ( 𝜑 → ( ( 𝐶 ∘ ( algSc ‘ 𝑈 ) ) ‘ ( 0g ‘ 𝑅 ) ) = ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ ( 0g ‘ 𝑅 ) ) ) )
57	3 14 11	mplsca	⊢ ( 𝜑 → 𝑅 = ( Scalar ‘ 𝑈 ) )
58	57	fveq2d	⊢ ( 𝜑 → ( 0g ‘ 𝑅 ) = ( 0g ‘ ( Scalar ‘ 𝑈 ) ) )
59	58	fveq2d	⊢ ( 𝜑 → ( ( algSc ‘ 𝑈 ) ‘ ( 0g ‘ 𝑅 ) ) = ( ( algSc ‘ 𝑈 ) ‘ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) )
60		eqid	⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
61	3	mplassa	⊢ ( ( ( 𝐼 ∖ 𝐽 ) ∈ V ∧ 𝑅 ∈ CRing ) → 𝑈 ∈ AssAlg )
62	14 11 61	syl2anc	⊢ ( 𝜑 → 𝑈 ∈ AssAlg )
63		assalmod	⊢ ( 𝑈 ∈ AssAlg → 𝑈 ∈ LMod )
64	62 63	syl	⊢ ( 𝜑 → 𝑈 ∈ LMod )
65		assaring	⊢ ( 𝑈 ∈ AssAlg → 𝑈 ∈ Ring )
66	62 65	syl	⊢ ( 𝜑 → 𝑈 ∈ Ring )
67	53 60 64 66	ascl0	⊢ ( 𝜑 → ( ( algSc ‘ 𝑈 ) ‘ ( 0g ‘ ( Scalar ‘ 𝑈 ) ) ) = ( 0g ‘ 𝑈 ) )
68	59 67	eqtrd	⊢ ( 𝜑 → ( ( algSc ‘ 𝑈 ) ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑈 ) )
69	68	fveq2d	⊢ ( 𝜑 → ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ ( 0g ‘ 𝑅 ) ) ) = ( 𝐶 ‘ ( 0g ‘ 𝑈 ) ) )
70	4 15 62	mplsca	⊢ ( 𝜑 → 𝑈 = ( Scalar ‘ 𝑇 ) )
71	70	fveq2d	⊢ ( 𝜑 → ( 0g ‘ 𝑈 ) = ( 0g ‘ ( Scalar ‘ 𝑇 ) ) )
72	71	fveq2d	⊢ ( 𝜑 → ( 𝐶 ‘ ( 0g ‘ 𝑈 ) ) = ( 𝐶 ‘ ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ) )
73		eqid	⊢ ( Scalar ‘ 𝑇 ) = ( Scalar ‘ 𝑇 )
74	3 4 14 15 11	selvval2lem1	⊢ ( 𝜑 → 𝑇 ∈ AssAlg )
75		assalmod	⊢ ( 𝑇 ∈ AssAlg → 𝑇 ∈ LMod )
76	74 75	syl	⊢ ( 𝜑 → 𝑇 ∈ LMod )
77		assaring	⊢ ( 𝑇 ∈ AssAlg → 𝑇 ∈ Ring )
78	74 77	syl	⊢ ( 𝜑 → 𝑇 ∈ Ring )
79	5 73 76 78	ascl0	⊢ ( 𝜑 → ( 𝐶 ‘ ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ) = ( 0g ‘ 𝑇 ) )
80		subrgsubg	⊢ ( ran 𝐷 ∈ ( SubRing ‘ 𝑇 ) → ran 𝐷 ∈ ( SubGrp ‘ 𝑇 ) )
81		eqid	⊢ ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑇 )
82	7 81	subg0	⊢ ( ran 𝐷 ∈ ( SubGrp ‘ 𝑇 ) → ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑆 ) )
83	22 80 82	3syl	⊢ ( 𝜑 → ( 0g ‘ 𝑇 ) = ( 0g ‘ 𝑆 ) )
84	79 83	eqtrd	⊢ ( 𝜑 → ( 𝐶 ‘ ( 0g ‘ ( Scalar ‘ 𝑇 ) ) ) = ( 0g ‘ 𝑆 ) )
85	69 72 84	3eqtrd	⊢ ( 𝜑 → ( 𝐶 ‘ ( ( algSc ‘ 𝑈 ) ‘ ( 0g ‘ 𝑅 ) ) ) = ( 0g ‘ 𝑆 ) )
86	51 56 85	3eqtrd	⊢ ( 𝜑 → ( 𝐷 ‘ ( 0g ‘ 𝑅 ) ) = ( 0g ‘ 𝑆 ) )
87	42 46 29 21 47 34 48 49 86	fsuppcor	⊢ ( 𝜑 → ( 𝐷 ∘ 𝐹 ) finSupp ( 0g ‘ 𝑆 ) )
88		eqid	⊢ ( 0g ‘ 𝑆 ) = ( 0g ‘ 𝑆 )
89	8 37 39 88 9	mplelbas	⊢ ( ( 𝐷 ∘ 𝐹 ) ∈ 𝑋 ↔ ( ( 𝐷 ∘ 𝐹 ) ∈ ( Base ‘ ( 𝐼 mPwSer 𝑆 ) ) ∧ ( 𝐷 ∘ 𝐹 ) finSupp ( 0g ‘ 𝑆 ) ) )
90	41 87 89	sylanbrc	⊢ ( 𝜑 → ( 𝐷 ∘ 𝐹 ) ∈ 𝑋 )