This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )