mplsubrglem

Description: Lemma for mplsubrg . (Contributed by Mario Carneiro, 9-Jan-2015) (Revised by AV, 18-Jul-2019)

	Ref	Expression
Hypotheses	mplsubg.s	$⊢ S = I mPwSer R$
	mplsubg.p	$⊢ P = I mPoly R$
	mplsubg.u	$⊢ U = {Base}_{P}$
	mplsubg.i	$⊢ φ \to I \in W$
	mpllss.r	$⊢ φ \to R \in Ring$
	mplsubrglem.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
	mplsubrglem.z	$⊢ \underset{˙}{0} = 0_{R}$
	mplsubrglem.p	$⊢ A = \circ_{f} + [{supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y)]$
	mplsubrglem.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	mplsubrglem.x	$⊢ φ \to X \in U$
	mplsubrglem.y	$⊢ φ \to Y \in U$
Assertion	mplsubrglem	$⊢ φ \to X \cdot_{S} Y \in U$

Proof

Step	Hyp	Ref	Expression
1		mplsubg.s	$⊢ S = I mPwSer R$
2		mplsubg.p	$⊢ P = I mPoly R$
3		mplsubg.u	$⊢ U = {Base}_{P}$
4		mplsubg.i	$⊢ φ \to I \in W$
5		mpllss.r	$⊢ φ \to R \in Ring$
6		mplsubrglem.d	$⊢ D = \{f \in ({ℕ_{0}}^{I}) \| f^{-1} [ℕ] \in Fin\}$
7		mplsubrglem.z	$⊢ \underset{˙}{0} = 0_{R}$
8		mplsubrglem.p	$⊢ A = \circ_{f} + [{supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y)]$
9		mplsubrglem.t	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
10		mplsubrglem.x	$⊢ φ \to X \in U$
11		mplsubrglem.y	$⊢ φ \to Y \in U$
12		eqid	$⊢ {Base}_{S} = {Base}_{S}$
13		eqid	$⊢ \cdot_{S} = \cdot_{S}$
14	2 1 3 12	mplbasss	$⊢ U \subseteq {Base}_{S}$
15	14 10	sselid	$⊢ φ \to X \in {Base}_{S}$
16	14 11	sselid	$⊢ φ \to Y \in {Base}_{S}$
17	1 12 13 5 15 16	psrmulcl	$⊢ φ \to X \cdot_{S} Y \in {Base}_{S}$
18		ovexd	$⊢ φ \to X \cdot_{S} Y \in V$
19	1 12	psrelbasfun	$⊢ X \cdot_{S} Y \in {Base}_{S} \to Fun (X \cdot_{S} Y)$
20	17 19	syl	$⊢ φ \to Fun (X \cdot_{S} Y)$
21	7	fvexi	$⊢ \underset{˙}{0} \in V$
22	21	a1i	$⊢ φ \to \underset{˙}{0} \in V$
23		df-ima	$⊢ \circ_{f} + [{supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y)] = ran ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))})$
24	8 23	eqtri	$⊢ A = ran ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))})$
25	2 1 12 7 3	mplelbas	$⊢ X \in U \leftrightarrow (X \in {Base}_{S} \land {finSupp}_{\underset{˙}{0}} (X))$
26	25	simprbi	$⊢ X \in U \to {finSupp}_{\underset{˙}{0}} (X)$
27	10 26	syl	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (X)$
28	2 1 12 7 3	mplelbas	$⊢ Y \in U \leftrightarrow (Y \in {Base}_{S} \land {finSupp}_{\underset{˙}{0}} (Y))$
29	28	simprbi	$⊢ Y \in U \to {finSupp}_{\underset{˙}{0}} (Y)$
30	11 29	syl	$⊢ φ \to {finSupp}_{\underset{˙}{0}} (Y)$
31		fsuppxpfi	$⊢ ({finSupp}_{\underset{˙}{0}} (X) \land {finSupp}_{\underset{˙}{0}} (Y)) \to {supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y) \in Fin$
32	27 30 31	syl2anc	$⊢ φ \to {supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y) \in Fin$
33		ofmres	$⊢ {\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))} = (f \in {supp}_{\underset{˙}{0}} (X), g \in {supp}_{\underset{˙}{0}} (Y) ⟼ f +_{f} g)$
34		ovex	$⊢ f +_{f} g \in V$
35	33 34	fnmpoi	$⊢ ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) Fn ({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))$
36		dffn4	$⊢ ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) Fn ({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y)) \leftrightarrow ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) : {supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y) \underset{onto}{⟶} ran ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))})$
37	35 36	mpbi	$⊢ ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) : {supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y) \underset{onto}{⟶} ran ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))})$
38		fofi	$⊢ ({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y) \in Fin \land ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) : {supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y) \underset{onto}{⟶} ran ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))})) \to ran ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) \in Fin$
39	32 37 38	sylancl	$⊢ φ \to ran ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) \in Fin$
40	24 39	eqeltrid	$⊢ φ \to A \in Fin$
41		eqid	$⊢ {Base}_{R} = {Base}_{R}$
42	1 41 6 12 17	psrelbas	$⊢ φ \to (X \cdot_{S} Y) : D ⟶ {Base}_{R}$
43	15	adantr	$⊢ (φ \land k \in (D ∖ A)) \to X \in {Base}_{S}$
44	16	adantr	$⊢ (φ \land k \in (D ∖ A)) \to Y \in {Base}_{S}$
45		eldifi	$⊢ k \in (D ∖ A) \to k \in D$
46	45	adantl	$⊢ (φ \land k \in (D ∖ A)) \to k \in D$
47	1 12 9 13 6 43 44 46	psrmulval	$⊢ (φ \land k \in (D ∖ A)) \to (X \cdot_{S} Y) (k) = \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \underset{˙}{\cdot} Y (k -_{f} x))$
48	5	ad2antrr	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to R \in Ring$
49	2 41 3 6 11	mplelf	$⊢ φ \to Y : D ⟶ {Base}_{R}$
50	49	ad2antrr	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y : D ⟶ {Base}_{R}$
51		ssrab2	$⊢ \{y \in D \| y \leq_{f} k\} \subseteq D$
52	46	adantr	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to k \in D$
53		simpr	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in \{y \in D \| y \leq_{f} k\}$
54		eqid	$⊢ \{y \in D \| y \leq_{f} k\} = \{y \in D \| y \leq_{f} k\}$
55	6 54	psrbagconcl	$⊢ (k \in D \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in \{y \in D \| y \leq_{f} k\}$
56	52 53 55	syl2anc	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in \{y \in D \| y \leq_{f} k\}$
57	51 56	sselid	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x \in D$
58	50 57	ffvelcdmd	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y (k -_{f} x) \in {Base}_{R}$
59	41 9 7	ringlz	$⊢ (R \in Ring \land Y (k -_{f} x) \in {Base}_{R}) \to \underset{˙}{0} \underset{˙}{\cdot} Y (k -_{f} x) = \underset{˙}{0}$
60	48 58 59	syl2anc	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to \underset{˙}{0} \underset{˙}{\cdot} Y (k -_{f} x) = \underset{˙}{0}$
61		oveq1	$⊢ X (x) = \underset{˙}{0} \to X (x) \underset{˙}{\cdot} Y (k -_{f} x) = \underset{˙}{0} \underset{˙}{\cdot} Y (k -_{f} x)$
62	61	eqeq1d	$⊢ X (x) = \underset{˙}{0} \to (X (x) \underset{˙}{\cdot} Y (k -_{f} x) = \underset{˙}{0} \leftrightarrow \underset{˙}{0} \underset{˙}{\cdot} Y (k -_{f} x) = \underset{˙}{0})$
63	60 62	syl5ibrcom	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to (X (x) = \underset{˙}{0} \to X (x) \underset{˙}{\cdot} Y (k -_{f} x) = \underset{˙}{0})$
64	2 41 3 6 10	mplelf	$⊢ φ \to X : D ⟶ {Base}_{R}$
65	64	ad2antrr	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to X : D ⟶ {Base}_{R}$
66	51 53	sselid	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to x \in D$
67	65 66	ffvelcdmd	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \in {Base}_{R}$
68	41 9 7	ringrz	$⊢ (R \in Ring \land X (x) \in {Base}_{R}) \to X (x) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
69	48 67 68	syl2anc	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0}$
70		oveq2	$⊢ Y (k -_{f} x) = \underset{˙}{0} \to X (x) \underset{˙}{\cdot} Y (k -_{f} x) = X (x) \underset{˙}{\cdot} \underset{˙}{0}$
71	70	eqeq1d	$⊢ Y (k -_{f} x) = \underset{˙}{0} \to (X (x) \underset{˙}{\cdot} Y (k -_{f} x) = \underset{˙}{0} \leftrightarrow X (x) \underset{˙}{\cdot} \underset{˙}{0} = \underset{˙}{0})$
72	69 71	syl5ibrcom	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to (Y (k -_{f} x) = \underset{˙}{0} \to X (x) \underset{˙}{\cdot} Y (k -_{f} x) = \underset{˙}{0})$
73	6	psrbagf	$⊢ x \in D \to x : I ⟶ ℕ_{0}$
74	66 73	syl	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to x : I ⟶ ℕ_{0}$
75	74	ffvelcdmda	$⊢ (((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \land n \in I) \to x (n) \in ℕ_{0}$
76	6	psrbagf	$⊢ k \in D \to k : I ⟶ ℕ_{0}$
77	52 76	syl	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to k : I ⟶ ℕ_{0}$
78	77	ffvelcdmda	$⊢ (((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \land n \in I) \to k (n) \in ℕ_{0}$
79		nn0cn	$⊢ x (n) \in ℕ_{0} \to x (n) \in ℂ$
80		nn0cn	$⊢ k (n) \in ℕ_{0} \to k (n) \in ℂ$
81		pncan3	$⊢ (x (n) \in ℂ \land k (n) \in ℂ) \to x (n) + k (n) - x (n) = k (n)$
82	79 80 81	syl2an	$⊢ (x (n) \in ℕ_{0} \land k (n) \in ℕ_{0}) \to x (n) + k (n) - x (n) = k (n)$
83	75 78 82	syl2anc	$⊢ (((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \land n \in I) \to x (n) + k (n) - x (n) = k (n)$
84	83	mpteq2dva	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to (n \in I ⟼ x (n) + k (n) - x (n)) = (n \in I ⟼ k (n))$
85	4	ad2antrr	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to I \in W$
86		ovexd	$⊢ (((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \land n \in I) \to k (n) - x (n) \in V$
87	74	feqmptd	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to x = (n \in I ⟼ x (n))$
88	77	feqmptd	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to k = (n \in I ⟼ k (n))$
89	85 78 75 88 87	offval2	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to k -_{f} x = (n \in I ⟼ k (n) - x (n))$
90	85 75 86 87 89	offval2	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to x +_{f} (k -_{f} x) = (n \in I ⟼ x (n) + k (n) - x (n))$
91	84 90 88	3eqtr4d	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to x +_{f} (k -_{f} x) = k$
92		simplr	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to k \in (D ∖ A)$
93	91 92	eqeltrd	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to x +_{f} (k -_{f} x) \in (D ∖ A)$
94	93	eldifbd	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to \neg x +_{f} (k -_{f} x) \in A$
95		ovres	$⊢ (x \in {supp}_{\underset{˙}{0}} (X) \land k -_{f} x \in {supp}_{\underset{˙}{0}} (Y)) \to x ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) (k -_{f} x) = x +_{f} (k -_{f} x)$
96		fnovrn	$⊢ (({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) Fn ({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y)) \land x \in {supp}_{\underset{˙}{0}} (X) \land k -_{f} x \in {supp}_{\underset{˙}{0}} (Y)) \to x ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) (k -_{f} x) \in ran ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))})$
97	96 24	eleqtrrdi	$⊢ (({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) Fn ({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y)) \land x \in {supp}_{\underset{˙}{0}} (X) \land k -_{f} x \in {supp}_{\underset{˙}{0}} (Y)) \to x ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) (k -_{f} x) \in A$
98	35 97	mp3an1	$⊢ (x \in {supp}_{\underset{˙}{0}} (X) \land k -_{f} x \in {supp}_{\underset{˙}{0}} (Y)) \to x ({\circ_{f} + ↾}_{({supp}_{\underset{˙}{0}} (X) \times {supp}_{\underset{˙}{0}} (Y))}) (k -_{f} x) \in A$
99	95 98	eqeltrrd	$⊢ (x \in {supp}_{\underset{˙}{0}} (X) \land k -_{f} x \in {supp}_{\underset{˙}{0}} (Y)) \to x +_{f} (k -_{f} x) \in A$
100	94 99	nsyl	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to \neg (x \in {supp}_{\underset{˙}{0}} (X) \land k -_{f} x \in {supp}_{\underset{˙}{0}} (Y))$
101		ianor	$⊢ \neg (x \in {supp}_{\underset{˙}{0}} (X) \land k -_{f} x \in {supp}_{\underset{˙}{0}} (Y)) \leftrightarrow (\neg x \in {supp}_{\underset{˙}{0}} (X) \lor \neg k -_{f} x \in {supp}_{\underset{˙}{0}} (Y))$
102	100 101	sylib	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to (\neg x \in {supp}_{\underset{˙}{0}} (X) \lor \neg k -_{f} x \in {supp}_{\underset{˙}{0}} (Y))$
103		eldif	$⊢ x \in (D ∖ {supp}_{\underset{˙}{0}} (X)) \leftrightarrow (x \in D \land \neg x \in {supp}_{\underset{˙}{0}} (X))$
104	103	baib	$⊢ x \in D \to (x \in (D ∖ {supp}_{\underset{˙}{0}} (X)) \leftrightarrow \neg x \in {supp}_{\underset{˙}{0}} (X))$
105	66 104	syl	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to (x \in (D ∖ {supp}_{\underset{˙}{0}} (X)) \leftrightarrow \neg x \in {supp}_{\underset{˙}{0}} (X))$
106		ssidd	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to X supp \underset{˙}{0} \subseteq X supp \underset{˙}{0}$
107		ovex	$⊢ {ℕ_{0}}^{I} \in V$
108	6 107	rabex2	$⊢ D \in V$
109	108	a1i	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to D \in V$
110	21	a1i	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to \underset{˙}{0} \in V$
111	65 106 109 110	suppssr	$⊢ (((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \land x \in (D ∖ {supp}_{\underset{˙}{0}} (X))) \to X (x) = \underset{˙}{0}$
112	111	ex	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to (x \in (D ∖ {supp}_{\underset{˙}{0}} (X)) \to X (x) = \underset{˙}{0})$
113	105 112	sylbird	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to (\neg x \in {supp}_{\underset{˙}{0}} (X) \to X (x) = \underset{˙}{0})$
114		eldif	$⊢ k -_{f} x \in (D ∖ {supp}_{\underset{˙}{0}} (Y)) \leftrightarrow (k -_{f} x \in D \land \neg k -_{f} x \in {supp}_{\underset{˙}{0}} (Y))$
115	114	baib	$⊢ k -_{f} x \in D \to (k -_{f} x \in (D ∖ {supp}_{\underset{˙}{0}} (Y)) \leftrightarrow \neg k -_{f} x \in {supp}_{\underset{˙}{0}} (Y))$
116	57 115	syl	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to (k -_{f} x \in (D ∖ {supp}_{\underset{˙}{0}} (Y)) \leftrightarrow \neg k -_{f} x \in {supp}_{\underset{˙}{0}} (Y))$
117		ssidd	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to Y supp \underset{˙}{0} \subseteq Y supp \underset{˙}{0}$
118	50 117 109 110	suppssr	$⊢ (((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \land k -_{f} x \in (D ∖ {supp}_{\underset{˙}{0}} (Y))) \to Y (k -_{f} x) = \underset{˙}{0}$
119	118	ex	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to (k -_{f} x \in (D ∖ {supp}_{\underset{˙}{0}} (Y)) \to Y (k -_{f} x) = \underset{˙}{0})$
120	116 119	sylbird	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to (\neg k -_{f} x \in {supp}_{\underset{˙}{0}} (Y) \to Y (k -_{f} x) = \underset{˙}{0})$
121	113 120	orim12d	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to ((\neg x \in {supp}_{\underset{˙}{0}} (X) \lor \neg k -_{f} x \in {supp}_{\underset{˙}{0}} (Y)) \to (X (x) = \underset{˙}{0} \lor Y (k -_{f} x) = \underset{˙}{0}))$
122	102 121	mpd	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to (X (x) = \underset{˙}{0} \lor Y (k -_{f} x) = \underset{˙}{0})$
123	63 72 122	mpjaod	$⊢ ((φ \land k \in (D ∖ A)) \land x \in \{y \in D \| y \leq_{f} k\}) \to X (x) \underset{˙}{\cdot} Y (k -_{f} x) = \underset{˙}{0}$
124	123	mpteq2dva	$⊢ (φ \land k \in (D ∖ A)) \to (x \in \{y \in D \| y \leq_{f} k\} ⟼ X (x) \underset{˙}{\cdot} Y (k -_{f} x)) = (x \in \{y \in D \| y \leq_{f} k\} ⟼ \underset{˙}{0})$
125	124	oveq2d	$⊢ (φ \land k \in (D ∖ A)) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} (X (x) \underset{˙}{\cdot} Y (k -_{f} x)) = \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} \underset{˙}{0}$
126	5	adantr	$⊢ (φ \land k \in (D ∖ A)) \to R \in Ring$
127		ringmnd	$⊢ R \in Ring \to R \in Mnd$
128	126 127	syl	$⊢ (φ \land k \in (D ∖ A)) \to R \in Mnd$
129	6	psrbaglefi	$⊢ k \in D \to \{y \in D \| y \leq_{f} k\} \in Fin$
130	46 129	syl	$⊢ (φ \land k \in (D ∖ A)) \to \{y \in D \| y \leq_{f} k\} \in Fin$
131	7	gsumz	$⊢ (R \in Mnd \land \{y \in D \| y \leq_{f} k\} \in Fin) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
132	128 130 131	syl2anc	$⊢ (φ \land k \in (D ∖ A)) \to \underset{x \in \{y \in D \| y \leq_{f} k\}}{\sum_{R}} \underset{˙}{0} = \underset{˙}{0}$
133	47 125 132	3eqtrd	$⊢ (φ \land k \in (D ∖ A)) \to (X \cdot_{S} Y) (k) = \underset{˙}{0}$
134	42 133	suppss	$⊢ φ \to (X \cdot_{S} Y) supp \underset{˙}{0} \subseteq A$
135		suppssfifsupp	$⊢ ((X \cdot_{S} Y \in V \land Fun (X \cdot_{S} Y) \land \underset{˙}{0} \in V) \land (A \in Fin \land (X \cdot_{S} Y) supp \underset{˙}{0} \subseteq A)) \to {finSupp}_{\underset{˙}{0}} ((X \cdot_{S} Y))$
136	18 20 22 40 134 135	syl32anc	$⊢ φ \to {finSupp}_{\underset{˙}{0}} ((X \cdot_{S} Y))$
137	2 1 12 7 3	mplelbas	$⊢ X \cdot_{S} Y \in U \leftrightarrow (X \cdot_{S} Y \in {Base}_{S} \land {finSupp}_{\underset{˙}{0}} ((X \cdot_{S} Y)))$
138	17 136 137	sylanbrc	$⊢ φ \to X \cdot_{S} Y \in U$

Metamath Proof Explorer

Theorem mplsubrglem

Proof