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	6	difexd	$⊢ φ \to I ∖ J \in V$
13		crngring	$⊢ R \in CRing \to R \in Ring$
14	7 13	syl	$⊢ φ \to R \in Ring$
15	1	mplring	$⊢ (I ∖ J \in V \land R \in Ring) \to U \in Ring$
16	12 14 15	syl2anc	$⊢ φ \to U \in Ring$
17	16	adantr	$⊢ (φ \land x \in J) \to U \in Ring$
18		simpr	$⊢ (φ \land x \in J) \to x \in J$
19	2 9 4 11 17 18	mvrcl	$⊢ (φ \land x \in J) \to (J mVar U) (x) \in E$
20	19	adantlr	$⊢ ((φ \land x \in I) \land x \in J) \to (J mVar U) (x) \in E$
21		eqid	$⊢ {Base}_{U} = {Base}_{U}$
22	2 4 21 3 10 16	mplasclf	$⊢ φ \to C : {Base}_{U} ⟶ E$
23	22	ad2antrr	$⊢ ((φ \land x \in I) \land \neg x \in J) \to C : {Base}_{U} ⟶ E$
24		eqid	$⊢ (I ∖ J) mVar R = (I ∖ J) mVar R$
25	12	ad2antrr	$⊢ ((φ \land x \in I) \land \neg x \in J) \to I ∖ J \in V$
26	14	ad2antrr	$⊢ ((φ \land x \in I) \land \neg x \in J) \to R \in Ring$
27		eldif	$⊢ x \in (I ∖ J) \leftrightarrow (x \in I \land \neg x \in J)$
28	27	biimpri	$⊢ (x \in I \land \neg x \in J) \to x \in (I ∖ J)$
29	28	adantll	$⊢ ((φ \land x \in I) \land \neg x \in J) \to x \in (I ∖ J)$
30	1 24 21 25 26 29	mvrcl	$⊢ ((φ \land x \in I) \land \neg x \in J) \to ((I ∖ J) mVar R) (x) \in {Base}_{U}$
31	23 30	ffvelrnd	$⊢ ((φ \land x \in I) \land \neg x \in J) \to C (((I ∖ J) mVar R) (x)) \in E$
32	20 31	ifclda	$⊢ (φ \land x \in I) \to if (x \in J, (J mVar U) (x), C (((I ∖ J) mVar R) (x))) \in E$
33	32 5	fmptd	$⊢ φ \to F : I ⟶ E$
34		fvexd	$⊢ φ \to {Base}_{T} \in V$
35	4 34	eqeltrid	$⊢ φ \to E \in V$
36	35 6	elmapd	$⊢ φ \to (F \in (E^{I}) \leftrightarrow F : I ⟶ E)$
37	33 36	mpbird	$⊢ φ \to F \in (E^{I})$

Metamath Proof Explorer

Theorem selvval2lem5

Proof