Theorem evlslem4

Description: The support of a tensor product of ring element families is contained in the product of the supports. (Contributed by Stefan O'Rear, 8-Mar-2015) (Revised by AV, 18-Jul-2019)

	Ref	Expression
Hypotheses	evlslem4.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	evlslem4.z	⊢ 0 = ( 0g ‘ 𝑅 )
	evlslem4.t	⊢ · = ( .r ‘ 𝑅 )
	evlslem4.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
	evlslem4.x	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑋 ∈ 𝐵 )
	evlslem4.y	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → 𝑌 ∈ 𝐵 )
	evlslem4.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
	evlslem4.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
Assertion	evlslem4	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 𝐽 ↦ ( 𝑋 · 𝑌 ) ) supp 0 ) ⊆ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) × ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		evlslem4.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		evlslem4.z	⊢ 0 = ( 0g ‘ 𝑅 )
3		evlslem4.t	⊢ · = ( .r ‘ 𝑅 )
4		evlslem4.r	⊢ ( 𝜑 → 𝑅 ∈ Ring )
5		evlslem4.x	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ) → 𝑋 ∈ 𝐵 )
6		evlslem4.y	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝐽 ) → 𝑌 ∈ 𝐵 )
7		evlslem4.i	⊢ ( 𝜑 → 𝐼 ∈ 𝑉 )
8		evlslem4.j	⊢ ( 𝜑 → 𝐽 ∈ 𝑊 )
9		simp2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) → 𝑥 ∈ 𝐼 )
10	5	3adant3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) → 𝑋 ∈ 𝐵 )
11		eqid	⊢ ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) = ( 𝑥 ∈ 𝐼 ↦ 𝑋 )
12	11	fvmpt2	⊢ ( ( 𝑥 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑥 ) = 𝑋 )
13	9 10 12	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑥 ) = 𝑋 )
14		simp3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) → 𝑦 ∈ 𝐽 )
15		eqid	⊢ ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) = ( 𝑦 ∈ 𝐽 ↦ 𝑌 )
16	15	fvmpt2	⊢ ( ( 𝑦 ∈ 𝐽 ∧ 𝑌 ∈ 𝐵 ) → ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑦 ) = 𝑌 )
17	14 6 16	3imp3i2an	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) → ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑦 ) = 𝑌 )
18	13 17	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑥 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑦 ) ) = ( 𝑋 · 𝑌 ) )
19	18	mpoeq3dva	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 𝐽 ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑥 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 𝐽 ↦ ( 𝑋 · 𝑌 ) ) )
20		nfcv	⊢ Ⅎ 𝑖 ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑥 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑦 ) )
21		nfcv	⊢ Ⅎ 𝑗 ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑥 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑦 ) )
22		nffvmpt1	⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑖 )
23		nfcv	⊢ Ⅎ 𝑥 ·
24		nfcv	⊢ Ⅎ 𝑥 ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑗 )
25	22 23 24	nfov	⊢ Ⅎ 𝑥 ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑖 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑗 ) )
26		nfcv	⊢ Ⅎ 𝑦 ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑖 )
27		nfcv	⊢ Ⅎ 𝑦 ·
28		nffvmpt1	⊢ Ⅎ 𝑦 ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑗 )
29	26 27 28	nfov	⊢ Ⅎ 𝑦 ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑖 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑗 ) )
30		fveq2	⊢ ( 𝑥 = 𝑖 → ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑖 ) )
31		fveq2	⊢ ( 𝑦 = 𝑗 → ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑦 ) = ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑗 ) )
32	30 31	oveqan12d	⊢ ( ( 𝑥 = 𝑖 ∧ 𝑦 = 𝑗 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑥 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑦 ) ) = ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑖 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑗 ) ) )
33	20 21 25 29 32	cbvmpo	⊢ ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 𝐽 ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑥 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑦 ) ) ) = ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑖 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑗 ) ) )
34		vex	⊢ 𝑖 ∈ V
35		vex	⊢ 𝑗 ∈ V
36	34 35	eqop2	⊢ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ ↔ ( 𝑧 ∈ ( V × V ) ∧ ( ( 1st ‘ 𝑧 ) = 𝑖 ∧ ( 2nd ‘ 𝑧 ) = 𝑗 ) ) )
37		fveq2	⊢ ( ( 1st ‘ 𝑧 ) = 𝑖 → ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) = ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑖 ) )
38		fveq2	⊢ ( ( 2nd ‘ 𝑧 ) = 𝑗 → ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) = ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑗 ) )
39	37 38	oveqan12d	⊢ ( ( ( 1st ‘ 𝑧 ) = 𝑖 ∧ ( 2nd ‘ 𝑧 ) = 𝑗 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) = ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑖 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑗 ) ) )
40	36 39	simplbiim	⊢ ( 𝑧 = ⟨ 𝑖 , 𝑗 ⟩ → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) = ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑖 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑗 ) ) )
41	40	mpompt	⊢ ( 𝑧 ∈ ( 𝐼 × 𝐽 ) ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) ) = ( 𝑖 ∈ 𝐼 , 𝑗 ∈ 𝐽 ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑖 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑗 ) ) )
42	33 41	eqtr4i	⊢ ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 𝐽 ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ 𝑥 ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ 𝑦 ) ) ) = ( 𝑧 ∈ ( 𝐼 × 𝐽 ) ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) )
43	19 42	eqtr3di	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 𝐽 ↦ ( 𝑋 · 𝑌 ) ) = ( 𝑧 ∈ ( 𝐼 × 𝐽 ) ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) ) )
44	43	oveq1d	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 𝐽 ↦ ( 𝑋 · 𝑌 ) ) supp 0 ) = ( ( 𝑧 ∈ ( 𝐼 × 𝐽 ) ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) ) supp 0 ) )
45		difxp	⊢ ( ( 𝐼 × 𝐽 ) ∖ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) × ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) = ( ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) ∪ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) )
46	45	eleq2i	⊢ ( 𝑧 ∈ ( ( 𝐼 × 𝐽 ) ∖ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) × ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ↔ 𝑧 ∈ ( ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) ∪ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ) )
47		elun	⊢ ( 𝑧 ∈ ( ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) ∪ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ) ↔ ( 𝑧 ∈ ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) ∨ 𝑧 ∈ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ) )
48	46 47	bitri	⊢ ( 𝑧 ∈ ( ( 𝐼 × 𝐽 ) ∖ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) × ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ↔ ( 𝑧 ∈ ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) ∨ 𝑧 ∈ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ) )
49		xp1st	⊢ ( 𝑧 ∈ ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) → ( 1st ‘ 𝑧 ) ∈ ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) )
50	5	fmpttd	⊢ ( 𝜑 → ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) : 𝐼 ⟶ 𝐵 )
51		ssidd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ⊆ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) )
52	2	fvexi	⊢ 0 ∈ V
53	52	a1i	⊢ ( 𝜑 → 0 ∈ V )
54	50 51 7 53	suppssr	⊢ ( ( 𝜑 ∧ ( 1st ‘ 𝑧 ) ∈ ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) = 0 )
55	49 54	sylan2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) = 0 )
56	55	oveq1d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) = ( 0 · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) )
57	6	fmpttd	⊢ ( 𝜑 → ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) : 𝐽 ⟶ 𝐵 )
58		xp2nd	⊢ ( 𝑧 ∈ ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) → ( 2nd ‘ 𝑧 ) ∈ 𝐽 )
59		ffvelcdm	⊢ ( ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) : 𝐽 ⟶ 𝐵 ∧ ( 2nd ‘ 𝑧 ) ∈ 𝐽 ) → ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ∈ 𝐵 )
60	57 58 59	syl2an	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) ) → ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ∈ 𝐵 )
61	1 3 2	ringlz	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ∈ 𝐵 ) → ( 0 · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) = 0 )
62	4 60 61	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) ) → ( 0 · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) = 0 )
63	56 62	eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) = 0 )
64		xp2nd	⊢ ( 𝑧 ∈ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) → ( 2nd ‘ 𝑧 ) ∈ ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) )
65		ssidd	⊢ ( 𝜑 → ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ⊆ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) )
66	57 65 8 53	suppssr	⊢ ( ( 𝜑 ∧ ( 2nd ‘ 𝑧 ) ∈ ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) → ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) = 0 )
67	64 66	sylan2	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ) → ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) = 0 )
68	67	oveq2d	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) = ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · 0 ) )
69		xp1st	⊢ ( 𝑧 ∈ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) → ( 1st ‘ 𝑧 ) ∈ 𝐼 )
70		ffvelcdm	⊢ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) : 𝐼 ⟶ 𝐵 ∧ ( 1st ‘ 𝑧 ) ∈ 𝐼 ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) ∈ 𝐵 )
71	50 69 70	syl2an	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ) → ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) ∈ 𝐵 )
72	1 3 2	ringrz	⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) ∈ 𝐵 ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · 0 ) = 0 )
73	4 71 72	syl2an2r	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · 0 ) = 0 )
74	68 73	eqtrd	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) = 0 )
75	63 74	jaodan	⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ( 𝐼 ∖ ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) ) × 𝐽 ) ∨ 𝑧 ∈ ( 𝐼 × ( 𝐽 ∖ ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) = 0 )
76	48 75	sylan2b	⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ( 𝐼 × 𝐽 ) ∖ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) × ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) ) ) → ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) = 0 )
77	7 8	xpexd	⊢ ( 𝜑 → ( 𝐼 × 𝐽 ) ∈ V )
78	76 77	suppss2	⊢ ( 𝜑 → ( ( 𝑧 ∈ ( 𝐼 × 𝐽 ) ↦ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) ‘ ( 1st ‘ 𝑧 ) ) · ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) ‘ ( 2nd ‘ 𝑧 ) ) ) ) supp 0 ) ⊆ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) × ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) )
79	44 78	eqsstrd	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐼 , 𝑦 ∈ 𝐽 ↦ ( 𝑋 · 𝑌 ) ) supp 0 ) ⊆ ( ( ( 𝑥 ∈ 𝐼 ↦ 𝑋 ) supp 0 ) × ( ( 𝑦 ∈ 𝐽 ↦ 𝑌 ) supp 0 ) ) )