Theorem selvval2lem5

Description: The fifth argument passed to evalSub is in the domain (a function I --> E ). (Contributed by SN, 22-Feb-2024)

	Ref	Expression
Hypotheses	selvval2lem5.u	⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
	selvval2lem5.t	⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
	selvval2lem5.c	⊢ 𝐶 = ( algSc ‘ 𝑇 )
	selvval2lem5.e	⊢ 𝐸 = ( Base ‘ 𝑇 )
	selvval2lem5.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) )
	selvval2lem5.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	selvval2lem5.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
	selvval2lem5.j	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
Assertion	selvval2lem5	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐸 ↑m 𝐼 ) )

Proof

Step	Hyp	Ref	Expression
1		selvval2lem5.u	⊢ 𝑈 = ( ( 𝐼 ∖ 𝐽 ) mPoly 𝑅 )
2		selvval2lem5.t	⊢ 𝑇 = ( 𝐽 mPoly 𝑈 )
3		selvval2lem5.c	⊢ 𝐶 = ( algSc ‘ 𝑇 )
4		selvval2lem5.e	⊢ 𝐸 = ( Base ‘ 𝑇 )
5		selvval2lem5.f	⊢ 𝐹 = ( 𝑥 ∈ 𝐼 ↦ if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) )
6		selvval2lem5.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
7		selvval2lem5.r	⊢ ( 𝜑 → 𝑅 ∈ CRing )
8		selvval2lem5.j	⊢ ( 𝜑 → 𝐽 ⊆ 𝐼 )
9		eqid	⊢ ( 𝐽 mVar 𝑈 ) = ( 𝐽 mVar 𝑈 )
10	6 8	ssexd	⊢ ( 𝜑 → 𝐽 ∈ V )
11	10	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝐽 ∈ V )
12	6	difexd	⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
13		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
14	7 13	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
15	1	mplring	⊢ ( ( ( 𝐼 ∖ 𝐽 ) ∈ V ∧ 𝑅 ∈ Ring ) → 𝑈 ∈ Ring )
16	12 14 15	syl2anc	⊢ ( 𝜑 → 𝑈 ∈ Ring )
17	16	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑈 ∈ Ring )
18		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐽 )
19	2 9 4 11 17 18	mvrcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) ∈ 𝐸 )
20	19	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) ∈ 𝐸 )
21		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
22	2 4 21 3 10 16	mplasclf	⊢ ( 𝜑 → 𝐶 : ( Base ‘ 𝑈 ) ⟶ 𝐸 )
23	22	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝐽 ) → 𝐶 : ( Base ‘ 𝑈 ) ⟶ 𝐸 )
24		eqid	⊢ ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) = ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 )
25	12	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝐽 ) → ( 𝐼 ∖ 𝐽 ) ∈ V )
26	14	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝐽 ) → 𝑅 ∈ Ring )
27		eldif	⊢ ( 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ↔ ( 𝑥 ∈ 𝐼 ∧ ¬ 𝑥 ∈ 𝐽 ) )
28	27	biimpri	⊢ ( ( 𝑥 ∈ 𝐼 ∧ ¬ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) )
29	28	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) )
30	1 24 21 25 26 29	mvrcl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝐽 ) → ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑈 ) )
31	23 30	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝐽 ) → ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ∈ 𝐸 )
32	20 31	ifclda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ∈ 𝐸 )
33	32 5	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐸 )
34		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑇 ) ∈ V )
35	4 34	eqeltrid	⊢ ( 𝜑 → 𝐸 ∈ V )
36	35 6	elmapd	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐸 ↑m 𝐼 ) ↔ 𝐹 : 𝐼 ⟶ 𝐸 ) )
37	33 36	mpbird	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐸 ↑m 𝐼 ) )