Metamath Proof Explorer

Theorem 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 ⊢ U = I ∖ J mPoly R
selvcllem5.t ⊢ T = J mPoly U
selvcllem5.c ⊢ C = algSc ⁡ T
selvcllem5.e ⊢ E = Base T
selvcllem5.f ⊢ F = x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
selvcllem5.i ⊢ φ → I ∈ V
selvcllem5.r ⊢ φ → R ∈ CRing
selvcllem5.j ⊢ φ → J ⊆ I
Assertion selvcllem5 ⊢ φ → F ∈ E I

Proof

Step Hyp Ref Expression
1 selvcllem5.u ⊢ U = I ∖ J mPoly R
2 selvcllem5.t ⊢ T = J mPoly U
3 selvcllem5.c ⊢ C = algSc ⁡ T
4 selvcllem5.e ⊢ E = Base T
5 selvcllem5.f ⊢ F = x ∈ I ⟼ if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x
6 selvcllem5.i ⊢ φ → I ∈ V
7 selvcllem5.r ⊢ φ → R ∈ CRing
8 selvcllem5.j ⊢ φ → J ⊆ I
9 4 fvexi ⊢ E ∈ V
10 9 a1i ⊢ φ → E ∈ V
11 eqid ⊢ J mVar U = J mVar U
12 6 8 ssexd ⊢ φ → J ∈ V
13 12 adantr ⊢ φ ∧ x ∈ J → J ∈ V
14 6 difexd ⊢ φ → I ∖ J ∈ V
15 7 crngringd ⊢ φ → R ∈ Ring
16 1 14 15 mplringd ⊢ φ → U ∈ Ring
17 16 adantr ⊢ φ ∧ x ∈ J → U ∈ Ring
18 simpr ⊢ φ ∧ x ∈ J → x ∈ J
19 2 11 4 13 17 18 mvrcl ⊢ φ ∧ x ∈ J → J mVar U ⁡ x ∈ E
20 19 adantlr ⊢ φ ∧ x ∈ I ∧ x ∈ J → J mVar U ⁡ x ∈ E
21 eqid ⊢ Base U = Base U
22 2 4 21 3 12 16 mplasclf ⊢ φ → C : Base U ⟶ E
23 22 ad2antrr ⊢ φ ∧ x ∈ I ∧ ¬ x ∈ J → C : Base U ⟶ E
24 eqid ⊢ I ∖ J mVar R = I ∖ J mVar R
25 14 ad2antrr ⊢ φ ∧ x ∈ I ∧ ¬ x ∈ J → I ∖ J ∈ V
26 15 ad2antrr ⊢ φ ∧ x ∈ I ∧ ¬ x ∈ J → R ∈ Ring
27 eldif ⊢ x ∈ I ∖ J ↔ x ∈ I ∧ ¬ x ∈ J
28 27 biimpri ⊢ x ∈ I ∧ ¬ x ∈ J → x ∈ I ∖ J
29 28 adantll ⊢ φ ∧ x ∈ I ∧ ¬ x ∈ J → x ∈ I ∖ J
30 1 24 21 25 26 29 mvrcl ⊢ φ ∧ x ∈ I ∧ ¬ x ∈ J → I ∖ J mVar R ⁡ x ∈ Base U
31 23 30 ffvelcdmd ⊢ φ ∧ x ∈ I ∧ ¬ x ∈ J → C ⁡ I ∖ J mVar R ⁡ x ∈ E
32 20 31 ifclda ⊢ φ ∧ x ∈ I → if x ∈ J J mVar U ⁡ x C ⁡ I ∖ J mVar R ⁡ x ∈ E
33 32 5 fmptd ⊢ φ → F : I ⟶ E
34 10 6 33 elmapdd ⊢ φ → F ∈ E I