Theorem mplsubrglem

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

	Ref	Expression
Hypotheses	mplsubg.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
	mplsubg.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
	mplsubg.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
	mplsubg.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
	mpllss.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	mplsubrglem.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
	mplsubrglem.z	⊢ 0 = ( 0g ‘ 𝑅 )
	mplsubrglem.p	⊢ 𝐴 = ( ∘f + “ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) )
	mplsubrglem.t	⊢ · = ( .r ‘ 𝑅 )
	mplsubrglem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
	mplsubrglem.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
Assertion	mplsubrglem	⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		mplsubg.s	⊢ 𝑆 = ( 𝐼 mPwSer 𝑅 )
2		mplsubg.p	⊢ 𝑃 = ( 𝐼 mPoly 𝑅 )
3		mplsubg.u	⊢ 𝑈 = ( Base ‘ 𝑃 )
4		mplsubg.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑊 )
5		mpllss.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
6		mplsubrglem.d	⊢ 𝐷 = { 𝑓 ∈ ( ℕ0 ↑m 𝐼 ) ∣ ( ◡ 𝑓 “ ℕ ) ∈ Fin }
7		mplsubrglem.z	⊢ 0 = ( 0g ‘ 𝑅 )
8		mplsubrglem.p	⊢ 𝐴 = ( ∘f + “ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) )
9		mplsubrglem.t	⊢ · = ( .r ‘ 𝑅 )
10		mplsubrglem.x	⊢ ( 𝜑 → 𝑋 ∈ 𝑈 )
11		mplsubrglem.y	⊢ ( 𝜑 → 𝑌 ∈ 𝑈 )
12		eqid	⊢ ( Base ‘ 𝑆 ) = ( Base ‘ 𝑆 )
13		eqid	⊢ ( .r ‘ 𝑆 ) = ( .r ‘ 𝑆 )
14	2 1 3 12	mplbasss	⊢ 𝑈 ⊆ ( Base ‘ 𝑆 )
15	14 10	sselid	⊢ ( 𝜑 → 𝑋 ∈ ( Base ‘ 𝑆 ) )
16	14 11	sselid	⊢ ( 𝜑 → 𝑌 ∈ ( Base ‘ 𝑆 ) )
17	1 12 13 5 15 16	psrmulcl	⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ ( Base ‘ 𝑆 ) )
18		ovexd	⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ V )
19	1 12	psrelbasfun	⊢ ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ ( Base ‘ 𝑆 ) → Fun ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) )
20	17 19	syl	⊢ ( 𝜑 → Fun ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) )
21	7	fvexi	⊢ 0 ∈ V
22	21	a1i	⊢ ( 𝜑 → 0 ∈ V )
23		df-ima	⊢ ( ∘f + “ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) = ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) )
24	8 23	eqtri	⊢ 𝐴 = ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) )
25	2 1 12 7 3	mplelbas	⊢ ( 𝑋 ∈ 𝑈 ↔ ( 𝑋 ∈ ( Base ‘ 𝑆 ) ∧ 𝑋 finSupp 0 ) )
26	25	simprbi	⊢ ( 𝑋 ∈ 𝑈 → 𝑋 finSupp 0 )
27	10 26	syl	⊢ ( 𝜑 → 𝑋 finSupp 0 )
28	2 1 12 7 3	mplelbas	⊢ ( 𝑌 ∈ 𝑈 ↔ ( 𝑌 ∈ ( Base ‘ 𝑆 ) ∧ 𝑌 finSupp 0 ) )
29	28	simprbi	⊢ ( 𝑌 ∈ 𝑈 → 𝑌 finSupp 0 )
30	11 29	syl	⊢ ( 𝜑 → 𝑌 finSupp 0 )
31		fsuppxpfi	⊢ ( ( 𝑋 finSupp 0 ∧ 𝑌 finSupp 0 ) → ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ∈ Fin )
32	27 30 31	syl2anc	⊢ ( 𝜑 → ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ∈ Fin )
33		ofmres	⊢ ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) = ( 𝑓 ∈ ( 𝑋 supp 0 ) , 𝑔 ∈ ( 𝑌 supp 0 ) ↦ ( 𝑓 ∘f + 𝑔 ) )
34		ovex	⊢ ( 𝑓 ∘f + 𝑔 ) ∈ V
35	33 34	fnmpoi	⊢ ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) Fn ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) )
36		dffn4	⊢ ( ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) Fn ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ↔ ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) : ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) –onto→ ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) )
37	35 36	mpbi	⊢ ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) : ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) –onto→ ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) )
38		fofi	⊢ ( ( ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ∈ Fin ∧ ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) : ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) –onto→ ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ) → ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ∈ Fin )
39	32 37 38	sylancl	⊢ ( 𝜑 → ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ∈ Fin )
40	24 39	eqeltrid	⊢ ( 𝜑 → 𝐴 ∈ Fin )
41		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
42	1 41 6 12 17	psrelbas	⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
43	15	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → 𝑋 ∈ ( Base ‘ 𝑆 ) )
44	16	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → 𝑌 ∈ ( Base ‘ 𝑆 ) )
45		eldifi	⊢ ( 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) → 𝑘 ∈ 𝐷 )
46	45	adantl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → 𝑘 ∈ 𝐷 )
47	1 12 9 13 6 43 44 46	psrmulval	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ‘ 𝑘 ) = ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) )
48	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑅 ∈ Ring )
49	2 41 3 6 11	mplelf	⊢ ( 𝜑 → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
50	49	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑌 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
51		ssrab2	⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ⊆ 𝐷
52	46	adantr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑘 ∈ 𝐷 )
53		simpr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
54		eqid	⊢ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } = { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 }
55	6 54	psrbagconcl	⊢ ( ( 𝑘 ∈ 𝐷 ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
56	52 53 55	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } )
57	51 56	sselid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 )
58	50 57	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) )
59	41 9 7	ringlz	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ∈ ( Base ‘ 𝑅 ) ) → ( 0 · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 )
60	48 58 59	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 0 · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 )
61		oveq1	⊢ ( ( 𝑋 ‘ 𝑥 ) = 0 → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( 0 · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) )
62	61	eqeq1d	⊢ ( ( 𝑋 ‘ 𝑥 ) = 0 → ( ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 ↔ ( 0 · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 ) )
63	60 62	syl5ibrcom	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) = 0 → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 ) )
64	2 41 3 6 10	mplelf	⊢ ( 𝜑 → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
65	64	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑋 : 𝐷 ⟶ ( Base ‘ 𝑅 ) )
66	51 53	sselid	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 ∈ 𝐷 )
67	65 66	ffvelrnd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) )
68	41 9 7	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ ( 𝑋 ‘ 𝑥 ) ∈ ( Base ‘ 𝑅 ) ) → ( ( 𝑋 ‘ 𝑥 ) · 0 ) = 0 )
69	48 67 68	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) · 0 ) = 0 )
70		oveq2	⊢ ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = ( ( 𝑋 ‘ 𝑥 ) · 0 ) )
71	70	eqeq1d	⊢ ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 → ( ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 ↔ ( ( 𝑋 ‘ 𝑥 ) · 0 ) = 0 ) )
72	69 71	syl5ibrcom	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 ) )
73	6	psrbagf	⊢ ( 𝑥 ∈ 𝐷 → 𝑥 : 𝐼 ⟶ ℕ0 )
74	66 73	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 : 𝐼 ⟶ ℕ0 )
75	74	ffvelrnda	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝑥 ‘ 𝑛 ) ∈ ℕ0 )
76	6	psrbagf	⊢ ( 𝑘 ∈ 𝐷 → 𝑘 : 𝐼 ⟶ ℕ0 )
77	52 76	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑘 : 𝐼 ⟶ ℕ0 )
78	77	ffvelrnda	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑛 ∈ 𝐼 ) → ( 𝑘 ‘ 𝑛 ) ∈ ℕ0 )
79		nn0cn	⊢ ( ( 𝑥 ‘ 𝑛 ) ∈ ℕ0 → ( 𝑥 ‘ 𝑛 ) ∈ ℂ )
80		nn0cn	⊢ ( ( 𝑘 ‘ 𝑛 ) ∈ ℕ0 → ( 𝑘 ‘ 𝑛 ) ∈ ℂ )
81		pncan3	⊢ ( ( ( 𝑥 ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑘 ‘ 𝑛 ) ∈ ℂ ) → ( ( 𝑥 ‘ 𝑛 ) + ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ) = ( 𝑘 ‘ 𝑛 ) )
82	79 80 81	syl2an	⊢ ( ( ( 𝑥 ‘ 𝑛 ) ∈ ℕ0 ∧ ( 𝑘 ‘ 𝑛 ) ∈ ℕ0 ) → ( ( 𝑥 ‘ 𝑛 ) + ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ) = ( 𝑘 ‘ 𝑛 ) )
83	75 78 82	syl2anc	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑥 ‘ 𝑛 ) + ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ) = ( 𝑘 ‘ 𝑛 ) )
84	83	mpteq2dva	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑛 ) + ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ) ) = ( 𝑛 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑛 ) ) )
85	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝐼 ∈ 𝑊 )
86		ovexd	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑛 ∈ 𝐼 ) → ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ∈ V )
87	74	feqmptd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑥 = ( 𝑛 ∈ 𝐼 ↦ ( 𝑥 ‘ 𝑛 ) ) )
88	77	feqmptd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑘 = ( 𝑛 ∈ 𝐼 ↦ ( 𝑘 ‘ 𝑛 ) ) )
89	85 78 75 88 87	offval2	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑘 ∘f − 𝑥 ) = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ) )
90	85 75 86 87 89	offval2	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑥 ∘f + ( 𝑘 ∘f − 𝑥 ) ) = ( 𝑛 ∈ 𝐼 ↦ ( ( 𝑥 ‘ 𝑛 ) + ( ( 𝑘 ‘ 𝑛 ) − ( 𝑥 ‘ 𝑛 ) ) ) ) )
91	84 90 88	3eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑥 ∘f + ( 𝑘 ∘f − 𝑥 ) ) = 𝑘 )
92		simplr	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) )
93	91 92	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑥 ∘f + ( 𝑘 ∘f − 𝑥 ) ) ∈ ( 𝐷 ∖ 𝐴 ) )
94	93	eldifbd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ¬ ( 𝑥 ∘f + ( 𝑘 ∘f − 𝑥 ) ) ∈ 𝐴 )
95		ovres	⊢ ( ( 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) → ( 𝑥 ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ( 𝑘 ∘f − 𝑥 ) ) = ( 𝑥 ∘f + ( 𝑘 ∘f − 𝑥 ) ) )
96		fnovrn	⊢ ( ( ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) Fn ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ∧ 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) → ( 𝑥 ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ( 𝑘 ∘f − 𝑥 ) ) ∈ ran ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) )
97	96 24	eleqtrrdi	⊢ ( ( ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) Fn ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ∧ 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) → ( 𝑥 ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ( 𝑘 ∘f − 𝑥 ) ) ∈ 𝐴 )
98	35 97	mp3an1	⊢ ( ( 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) → ( 𝑥 ( ∘f + ↾ ( ( 𝑋 supp 0 ) × ( 𝑌 supp 0 ) ) ) ( 𝑘 ∘f − 𝑥 ) ) ∈ 𝐴 )
99	95 98	eqeltrrd	⊢ ( ( 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) → ( 𝑥 ∘f + ( 𝑘 ∘f − 𝑥 ) ) ∈ 𝐴 )
100	94 99	nsyl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ¬ ( 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) )
101		ianor	⊢ ( ¬ ( 𝑥 ∈ ( 𝑋 supp 0 ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) ↔ ( ¬ 𝑥 ∈ ( 𝑋 supp 0 ) ∨ ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) )
102	100 101	sylib	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ¬ 𝑥 ∈ ( 𝑋 supp 0 ) ∨ ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) )
103		eldif	⊢ ( 𝑥 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ↔ ( 𝑥 ∈ 𝐷 ∧ ¬ 𝑥 ∈ ( 𝑋 supp 0 ) ) )
104	103	baib	⊢ ( 𝑥 ∈ 𝐷 → ( 𝑥 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ↔ ¬ 𝑥 ∈ ( 𝑋 supp 0 ) ) )
105	66 104	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑥 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ↔ ¬ 𝑥 ∈ ( 𝑋 supp 0 ) ) )
106		ssidd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑋 supp 0 ) ⊆ ( 𝑋 supp 0 ) )
107		ovex	⊢ ( ℕ0 ↑m 𝐼 ) ∈ V
108	6 107	rabex2	⊢ 𝐷 ∈ V
109	108	a1i	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 𝐷 ∈ V )
110	21	a1i	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → 0 ∈ V )
111	65 106 109 110	suppssr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ 𝑥 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) ) → ( 𝑋 ‘ 𝑥 ) = 0 )
112	111	ex	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑥 ∈ ( 𝐷 ∖ ( 𝑋 supp 0 ) ) → ( 𝑋 ‘ 𝑥 ) = 0 ) )
113	105 112	sylbird	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ¬ 𝑥 ∈ ( 𝑋 supp 0 ) → ( 𝑋 ‘ 𝑥 ) = 0 ) )
114		eldif	⊢ ( ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝐷 ∖ ( 𝑌 supp 0 ) ) ↔ ( ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 ∧ ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) )
115	114	baib	⊢ ( ( 𝑘 ∘f − 𝑥 ) ∈ 𝐷 → ( ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝐷 ∖ ( 𝑌 supp 0 ) ) ↔ ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) )
116	57 115	syl	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝐷 ∖ ( 𝑌 supp 0 ) ) ↔ ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) )
117		ssidd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( 𝑌 supp 0 ) ⊆ ( 𝑌 supp 0 ) )
118	50 117 109 110	suppssr	⊢ ( ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) ∧ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝐷 ∖ ( 𝑌 supp 0 ) ) ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 )
119	118	ex	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝐷 ∖ ( 𝑌 supp 0 ) ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 ) )
120	116 119	sylbird	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) → ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 ) )
121	113 120	orim12d	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( ¬ 𝑥 ∈ ( 𝑋 supp 0 ) ∨ ¬ ( 𝑘 ∘f − 𝑥 ) ∈ ( 𝑌 supp 0 ) ) → ( ( 𝑋 ‘ 𝑥 ) = 0 ∨ ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 ) ) )
122	102 121	mpd	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) = 0 ∨ ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) = 0 ) )
123	63 72 122	mpjaod	⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) ∧ 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ) → ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) = 0 )
124	123	mpteq2dva	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) = ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ 0 ) )
125	124	oveq2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ ( ( 𝑋 ‘ 𝑥 ) · ( 𝑌 ‘ ( 𝑘 ∘f − 𝑥 ) ) ) ) ) = ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ 0 ) ) )
126	5	adantr	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → 𝑅 ∈ Ring )
127		ringmnd	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Mnd )
128	126 127	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → 𝑅 ∈ Mnd )
129	6	psrbaglefi	⊢ ( 𝑘 ∈ 𝐷 → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
130	46 129	syl	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin )
131	7	gsumz	⊢ ( ( 𝑅 ∈ Mnd ∧ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ∈ Fin ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ 0 ) ) = 0 )
132	128 130 131	syl2anc	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → ( 𝑅 Σg ( 𝑥 ∈ { 𝑦 ∈ 𝐷 ∣ 𝑦 ∘r ≤ 𝑘 } ↦ 0 ) ) = 0 )
133	47 125 132	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝐷 ∖ 𝐴 ) ) → ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ‘ 𝑘 ) = 0 )
134	42 133	suppss	⊢ ( 𝜑 → ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) supp 0 ) ⊆ 𝐴 )
135		suppssfifsupp	⊢ ( ( ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ V ∧ Fun ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∧ 0 ∈ V ) ∧ ( 𝐴 ∈ Fin ∧ ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) supp 0 ) ⊆ 𝐴 ) ) → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) finSupp 0 )
136	18 20 22 40 134 135	syl32anc	⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) finSupp 0 )
137	2 1 12 7 3	mplelbas	⊢ ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ 𝑈 ↔ ( ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ ( Base ‘ 𝑆 ) ∧ ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) finSupp 0 ) )
138	17 136 137	sylanbrc	⊢ ( 𝜑 → ( 𝑋 ( .r ‘ 𝑆 ) 𝑌 ) ∈ 𝑈 )