Step | Hyp | Ref
| Expression |
1 | | simp2 1136 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑥 ∈ 𝐼) |
2 | | evlslem4.x |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑋 ∈ 𝐵) |
3 | 2 | 3adant3 1131 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑋 ∈ 𝐵) |
4 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐼 ↦ 𝑋) = (𝑥 ∈ 𝐼 ↦ 𝑋) |
5 | 4 | fvmpt2 6886 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) = 𝑋) |
6 | 1, 3, 5 | syl2anc 584 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) = 𝑋) |
7 | | simp3 1137 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑦 ∈ 𝐽) |
8 | | evlslem4.y |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑌 ∈ 𝐵) |
9 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐽 ↦ 𝑌) = (𝑦 ∈ 𝐽 ↦ 𝑌) |
10 | 9 | fvmpt2 6886 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐽 ∧ 𝑌 ∈ 𝐵) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦) = 𝑌) |
11 | 7, 8, 10 | 3imp3i2an 1344 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦) = 𝑌) |
12 | 6, 11 | oveq12d 7293 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) = (𝑋 · 𝑌)) |
13 | 12 | mpoeq3dva 7352 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) = (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌))) |
14 | | nfcv 2907 |
. . . . . 6
⊢
Ⅎ𝑖(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) |
15 | | nfcv 2907 |
. . . . . 6
⊢
Ⅎ𝑗(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) |
16 | | nffvmpt1 6785 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) |
17 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑥
· |
18 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) |
19 | 16, 17, 18 | nfov 7305 |
. . . . . 6
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
20 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑦((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) |
21 | | nfcv 2907 |
. . . . . . 7
⊢
Ⅎ𝑦
· |
22 | | nffvmpt1 6785 |
. . . . . . 7
⊢
Ⅎ𝑦((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) |
23 | 20, 21, 22 | nfov 7305 |
. . . . . 6
⊢
Ⅎ𝑦(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
24 | | fveq2 6774 |
. . . . . . 7
⊢ (𝑥 = 𝑖 → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖)) |
25 | | fveq2 6774 |
. . . . . . 7
⊢ (𝑦 = 𝑗 → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦) = ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
26 | 24, 25 | oveqan12d 7294 |
. . . . . 6
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
27 | 14, 15, 19, 23, 26 | cbvmpo 7369 |
. . . . 5
⊢ (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
28 | | vex 3436 |
. . . . . . . 8
⊢ 𝑖 ∈ V |
29 | | vex 3436 |
. . . . . . . 8
⊢ 𝑗 ∈ V |
30 | 28, 29 | eqop2 7874 |
. . . . . . 7
⊢ (𝑧 = 〈𝑖, 𝑗〉 ↔ (𝑧 ∈ (V × V) ∧ ((1st
‘𝑧) = 𝑖 ∧ (2nd
‘𝑧) = 𝑗))) |
31 | | fveq2 6774 |
. . . . . . . 8
⊢
((1st ‘𝑧) = 𝑖 → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) = ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖)) |
32 | | fveq2 6774 |
. . . . . . . 8
⊢
((2nd ‘𝑧) = 𝑗 → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) = ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
33 | 31, 32 | oveqan12d 7294 |
. . . . . . 7
⊢
(((1st ‘𝑧) = 𝑖 ∧ (2nd ‘𝑧) = 𝑗) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
34 | 30, 33 | simplbiim 505 |
. . . . . 6
⊢ (𝑧 = 〈𝑖, 𝑗〉 → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
35 | 34 | mpompt 7388 |
. . . . 5
⊢ (𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
36 | 27, 35 | eqtr4i 2769 |
. . . 4
⊢ (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) = (𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) |
37 | 13, 36 | eqtr3di 2793 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)) = (𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))))) |
38 | 37 | oveq1d 7290 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)) supp 0 ) = ((𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) supp 0 )) |
39 | | difxp 6067 |
. . . . . 6
⊢ ((𝐼 × 𝐽) ∖ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) = (((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∪ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) |
40 | 39 | eleq2i 2830 |
. . . . 5
⊢ (𝑧 ∈ ((𝐼 × 𝐽) ∖ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) ↔ 𝑧 ∈ (((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∪ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))))) |
41 | | elun 4083 |
. . . . 5
⊢ (𝑧 ∈ (((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∪ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) ↔ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∨ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))))) |
42 | 40, 41 | bitri 274 |
. . . 4
⊢ (𝑧 ∈ ((𝐼 × 𝐽) ∖ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) ↔ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∨ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))))) |
43 | | xp1st 7863 |
. . . . . . . 8
⊢ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) → (1st
‘𝑧) ∈ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ))) |
44 | 2 | fmpttd 6989 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑋):𝐼⟶𝐵) |
45 | | ssidd 3944 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) ⊆ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) |
46 | | evlslem4.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
47 | | evlslem4.z |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑅) |
48 | 47 | fvexi 6788 |
. . . . . . . . . 10
⊢ 0 ∈
V |
49 | 48 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ V) |
50 | 44, 45, 46, 49 | suppssr 8012 |
. . . . . . . 8
⊢ ((𝜑 ∧ (1st
‘𝑧) ∈ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ))) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) = 0 ) |
51 | 43, 50 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) = 0 ) |
52 | 51 | oveq1d 7290 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = ( 0 · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) |
53 | | evlslem4.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
54 | 8 | fmpttd 6989 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ 𝑌):𝐽⟶𝐵) |
55 | | xp2nd 7864 |
. . . . . . . 8
⊢ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) → (2nd
‘𝑧) ∈ 𝐽) |
56 | | ffvelrn 6959 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝐽 ↦ 𝑌):𝐽⟶𝐵 ∧ (2nd ‘𝑧) ∈ 𝐽) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) ∈ 𝐵) |
57 | 54, 55, 56 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) ∈ 𝐵) |
58 | | evlslem4.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
59 | | evlslem4.t |
. . . . . . . 8
⊢ · =
(.r‘𝑅) |
60 | 58, 59, 47 | ringlz 19826 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) ∈ 𝐵) → ( 0 · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
61 | 53, 57, 60 | syl2an2r 682 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → ( 0 · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
62 | 52, 61 | eqtrd 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
63 | | xp2nd 7864 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) → (2nd
‘𝑧) ∈ (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |
64 | | ssidd 3944 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ) ⊆ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) |
65 | | evlslem4.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ 𝑊) |
66 | 54, 64, 65, 49 | suppssr 8012 |
. . . . . . . 8
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈ (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) = 0 ) |
67 | 63, 66 | sylan2 593 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) = 0 ) |
68 | 67 | oveq2d 7291 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · 0 )) |
69 | | xp1st 7863 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) → (1st
‘𝑧) ∈ 𝐼) |
70 | | ffvelrn 6959 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐼 ↦ 𝑋):𝐼⟶𝐵 ∧ (1st ‘𝑧) ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) ∈ 𝐵) |
71 | 44, 69, 70 | syl2an 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) ∈ 𝐵) |
72 | 58, 59, 47 | ringrz 19827 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) ∈ 𝐵) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · 0 ) = 0 ) |
73 | 53, 71, 72 | syl2an2r 682 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · 0 ) = 0 ) |
74 | 68, 73 | eqtrd 2778 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
75 | 62, 74 | jaodan 955 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∨ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
76 | 42, 75 | sylan2b 594 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 × 𝐽) ∖ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
77 | 46, 65 | xpexd 7601 |
. . 3
⊢ (𝜑 → (𝐼 × 𝐽) ∈ V) |
78 | 76, 77 | suppss2 8016 |
. 2
⊢ (𝜑 → ((𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) supp 0 ) ⊆ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |
79 | 38, 78 | eqsstrd 3959 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)) supp 0 ) ⊆ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |