selvcllem5

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

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

Proof

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

Metamath Proof Explorer

Theorem selvcllem5

Proof