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	$⊢ U = (I ∖ J) mPoly R$
	selvval2lem5.t	$⊢ T = J mPoly U$
	selvval2lem5.c	$⊢ C = algSc (T)$
	selvval2lem5.e	$⊢ E = {Base}_{T}$
	selvval2lem5.f	$⊢ F = (x \in I ⟼ if (x \in J, (J mVar U) (x), C (((I ∖ J) mVar R) (x))))$
	selvval2lem5.i	$⊢ φ \to I \in V$
	selvval2lem5.r	$⊢ φ \to R \in CRing$
	selvval2lem5.j	$⊢ φ \to J \subseteq I$
Assertion	selvval2lem5	$⊢ φ \to F \in (E^{I})$

Proof

Step	Hyp	Ref	Expression
1		selvval2lem5.u	$⊢ U = (I ∖ J) mPoly R$
2		selvval2lem5.t	$⊢ T = J mPoly U$
3		selvval2lem5.c	$⊢ C = algSc (T)$
4		selvval2lem5.e	$⊢ E = {Base}_{T}$
5		selvval2lem5.f	$⊢ F = (x \in I ⟼ if (x \in J, (J mVar U) (x), C (((I ∖ J) mVar R) (x))))$
6		selvval2lem5.i	$⊢ φ \to I \in V$
7		selvval2lem5.r	$⊢ φ \to R \in CRing$
8		selvval2lem5.j	$⊢ φ \to J \subseteq I$
9		eqid	$⊢ J mVar U = J mVar U$
10	6 8	ssexd	$⊢ φ \to J \in V$
11	10	adantr	$⊢ (φ \land x \in J) \to J \in V$
12		difexg	$⊢ I \in V \to I ∖ J \in V$
13	6 12	syl	$⊢ φ \to I ∖ J \in V$
14		crngring	$⊢ R \in CRing \to R \in Ring$
15	7 14	syl	$⊢ φ \to R \in Ring$
16	1	mplring	$⊢ (I ∖ J \in V \land R \in Ring) \to U \in Ring$
17	13 15 16	syl2anc	$⊢ φ \to U \in Ring$
18	17	adantr	$⊢ (φ \land x \in J) \to U \in Ring$
19		simpr	$⊢ (φ \land x \in J) \to x \in J$
20	2 9 4 11 18 19	mvrcl	$⊢ (φ \land x \in J) \to (J mVar U) (x) \in E$
21	20	adantlr	$⊢ ((φ \land x \in I) \land x \in J) \to (J mVar U) (x) \in E$
22		eqid	$⊢ {Base}_{U} = {Base}_{U}$
23	2 4 22 3 10 17	mplasclf	$⊢ φ \to C : {Base}_{U} ⟶ E$
24	23	ad2antrr	$⊢ ((φ \land x \in I) \land \neg x \in J) \to C : {Base}_{U} ⟶ E$
25		eqid	$⊢ (I ∖ J) mVar R = (I ∖ J) mVar R$
26	13	ad2antrr	$⊢ ((φ \land x \in I) \land \neg x \in J) \to I ∖ J \in V$
27	15	ad2antrr	$⊢ ((φ \land x \in I) \land \neg x \in J) \to R \in Ring$
28		eldif	$⊢ x \in (I ∖ J) \leftrightarrow (x \in I \land \neg x \in J)$
29	28	biimpri	$⊢ (x \in I \land \neg x \in J) \to x \in (I ∖ J)$
30	29	adantll	$⊢ ((φ \land x \in I) \land \neg x \in J) \to x \in (I ∖ J)$
31	1 25 22 26 27 30	mvrcl	$⊢ ((φ \land x \in I) \land \neg x \in J) \to ((I ∖ J) mVar R) (x) \in {Base}_{U}$
32	24 31	ffvelrnd	$⊢ ((φ \land x \in I) \land \neg x \in J) \to C (((I ∖ J) mVar R) (x)) \in E$
33	21 32	ifclda	$⊢ (φ \land x \in I) \to if (x \in J, (J mVar U) (x), C (((I ∖ J) mVar R) (x))) \in E$
34	33 5	fmptd	$⊢ φ \to F : I ⟶ E$
35		fvexd	$⊢ φ \to {Base}_{T} \in V$
36	4 35	eqeltrid	$⊢ φ \to E \in V$
37	36 6	elmapd	$⊢ φ \to (F \in (E^{I}) \leftrightarrow F : I ⟶ E)$
38	34 37	mpbird	$⊢ φ \to F \in (E^{I})$

Metamath Proof Explorer

Theorem selvval2lem5

Proof