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		difexg	⊢ ( 𝐼 ∈ 𝑉 → ( 𝐼 ∖ 𝐽 ) ∈ V )
13	6 12	syl	⊢ ( 𝜑 → ( 𝐼 ∖ 𝐽 ) ∈ V )
14		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
15	7 14	syl	⊢ ( 𝜑 → 𝑅 ∈ Ring )
16	1	mplring	⊢ ( ( ( 𝐼 ∖ 𝐽 ) ∈ V ∧ 𝑅 ∈ Ring ) → 𝑈 ∈ Ring )
17	13 15 16	syl2anc	⊢ ( 𝜑 → 𝑈 ∈ Ring )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑈 ∈ Ring )
19		simpr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ 𝐽 )
20	2 9 4 11 18 19	mvrcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) ∈ 𝐸 )
21	20	adantlr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ 𝑥 ∈ 𝐽 ) → ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) ∈ 𝐸 )
22		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
23	2 4 22 3 10 17	mplasclf	⊢ ( 𝜑 → 𝐶 : ( Base ‘ 𝑈 ) ⟶ 𝐸 )
24	23	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝐽 ) → 𝐶 : ( Base ‘ 𝑈 ) ⟶ 𝐸 )
25		eqid	⊢ ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) = ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 )
26	13	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝐽 ) → ( 𝐼 ∖ 𝐽 ) ∈ V )
27	15	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝐽 ) → 𝑅 ∈ Ring )
28		eldif	⊢ ( 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) ↔ ( 𝑥 ∈ 𝐼 ∧ ¬ 𝑥 ∈ 𝐽 ) )
29	28	biimpri	⊢ ( ( 𝑥 ∈ 𝐼 ∧ ¬ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) )
30	29	adantll	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝐽 ) → 𝑥 ∈ ( 𝐼 ∖ 𝐽 ) )
31	1 25 22 26 27 30	mvrcl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝐽 ) → ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝑈 ) )
32	24 31	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) ∧ ¬ 𝑥 ∈ 𝐽 ) → ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ∈ 𝐸 )
33	21 32	ifclda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → if ( 𝑥 ∈ 𝐽 , ( ( 𝐽 mVar 𝑈 ) ‘ 𝑥 ) , ( 𝐶 ‘ ( ( ( 𝐼 ∖ 𝐽 ) mVar 𝑅 ) ‘ 𝑥 ) ) ) ∈ 𝐸 )
34	33 5	fmptd	⊢ ( 𝜑 → 𝐹 : 𝐼 ⟶ 𝐸 )
35		fvexd	⊢ ( 𝜑 → ( Base ‘ 𝑇 ) ∈ V )
36	4 35	eqeltrid	⊢ ( 𝜑 → 𝐸 ∈ V )
37	36 6	elmapd	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐸 ↑m 𝐼 ) ↔ 𝐹 : 𝐼 ⟶ 𝐸 ) )
38	34 37	mpbird	⊢ ( 𝜑 → 𝐹 ∈ ( 𝐸 ↑m 𝐼 ) )