Step | Hyp | Ref
| Expression |
1 | | nfcv 2899 |
. . . . . 6
⊢
Ⅎ𝑖(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) |
2 | | nfcv 2899 |
. . . . . 6
⊢
Ⅎ𝑗(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) |
3 | | nffvmpt1 6679 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) |
4 | | nfcv 2899 |
. . . . . . 7
⊢
Ⅎ𝑥
· |
5 | | nfcv 2899 |
. . . . . . 7
⊢
Ⅎ𝑥((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) |
6 | 3, 4, 5 | nfov 7194 |
. . . . . 6
⊢
Ⅎ𝑥(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
7 | | nfcv 2899 |
. . . . . . 7
⊢
Ⅎ𝑦((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) |
8 | | nfcv 2899 |
. . . . . . 7
⊢
Ⅎ𝑦
· |
9 | | nffvmpt1 6679 |
. . . . . . 7
⊢
Ⅎ𝑦((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗) |
10 | 7, 8, 9 | nfov 7194 |
. . . . . 6
⊢
Ⅎ𝑦(((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
11 | | fveq2 6668 |
. . . . . . 7
⊢ (𝑥 = 𝑖 → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) = ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖)) |
12 | | fveq2 6668 |
. . . . . . 7
⊢ (𝑦 = 𝑗 → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦) = ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
13 | 11, 12 | oveqan12d 7183 |
. . . . . 6
⊢ ((𝑥 = 𝑖 ∧ 𝑦 = 𝑗) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
14 | 1, 2, 6, 10, 13 | cbvmpo 7256 |
. . . . 5
⊢ (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
15 | | vex 3401 |
. . . . . . . 8
⊢ 𝑖 ∈ V |
16 | | vex 3401 |
. . . . . . . 8
⊢ 𝑗 ∈ V |
17 | 15, 16 | eqop2 7750 |
. . . . . . 7
⊢ (𝑧 = 〈𝑖, 𝑗〉 ↔ (𝑧 ∈ (V × V) ∧ ((1st
‘𝑧) = 𝑖 ∧ (2nd
‘𝑧) = 𝑗))) |
18 | | fveq2 6668 |
. . . . . . . 8
⊢
((1st ‘𝑧) = 𝑖 → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) = ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖)) |
19 | | fveq2 6668 |
. . . . . . . 8
⊢
((2nd ‘𝑧) = 𝑗 → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) = ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗)) |
20 | 18, 19 | oveqan12d 7183 |
. . . . . . 7
⊢
(((1st ‘𝑧) = 𝑖 ∧ (2nd ‘𝑧) = 𝑗) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
21 | 17, 20 | simplbiim 508 |
. . . . . 6
⊢ (𝑧 = 〈𝑖, 𝑗〉 → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
22 | 21 | mpompt 7274 |
. . . . 5
⊢ (𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) = (𝑖 ∈ 𝐼, 𝑗 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑖) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑗))) |
23 | 14, 22 | eqtr4i 2764 |
. . . 4
⊢ (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) = (𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) |
24 | | simp2 1138 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑥 ∈ 𝐼) |
25 | | evlslem4.x |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼) → 𝑋 ∈ 𝐵) |
26 | 25 | 3adant3 1133 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑋 ∈ 𝐵) |
27 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐼 ↦ 𝑋) = (𝑥 ∈ 𝐼 ↦ 𝑋) |
28 | 27 | fvmpt2 6780 |
. . . . . . 7
⊢ ((𝑥 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) = 𝑋) |
29 | 24, 26, 28 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) = 𝑋) |
30 | | simp3 1139 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → 𝑦 ∈ 𝐽) |
31 | | evlslem4.y |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐽) → 𝑌 ∈ 𝐵) |
32 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑦 ∈ 𝐽 ↦ 𝑌) = (𝑦 ∈ 𝐽 ↦ 𝑌) |
33 | 32 | fvmpt2 6780 |
. . . . . . 7
⊢ ((𝑦 ∈ 𝐽 ∧ 𝑌 ∈ 𝐵) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦) = 𝑌) |
34 | 30, 31, 33 | 3imp3i2an 1346 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦) = 𝑌) |
35 | 29, 34 | oveq12d 7182 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐼 ∧ 𝑦 ∈ 𝐽) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦)) = (𝑋 · 𝑌)) |
36 | 35 | mpoeq3dva 7239 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘𝑥) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘𝑦))) = (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌))) |
37 | 23, 36 | syl5reqr 2788 |
. . 3
⊢ (𝜑 → (𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)) = (𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))))) |
38 | 37 | oveq1d 7179 |
. 2
⊢ (𝜑 → ((𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)) supp 0 ) = ((𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) supp 0 )) |
39 | | difxp 5990 |
. . . . . 6
⊢ ((𝐼 × 𝐽) ∖ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) = (((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∪ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) |
40 | 39 | eleq2i 2824 |
. . . . 5
⊢ (𝑧 ∈ ((𝐼 × 𝐽) ∖ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) ↔ 𝑧 ∈ (((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∪ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))))) |
41 | | elun 4037 |
. . . . 5
⊢ (𝑧 ∈ (((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∪ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) ↔ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∨ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))))) |
42 | 40, 41 | bitri 278 |
. . . 4
⊢ (𝑧 ∈ ((𝐼 × 𝐽) ∖ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) ↔ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∨ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))))) |
43 | | xp1st 7739 |
. . . . . . . 8
⊢ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) → (1st
‘𝑧) ∈ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ))) |
44 | 25 | fmpttd 6883 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝐼 ↦ 𝑋):𝐼⟶𝐵) |
45 | | ssidd 3898 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) ⊆ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) |
46 | | evlslem4.i |
. . . . . . . . 9
⊢ (𝜑 → 𝐼 ∈ 𝑉) |
47 | | evlslem4.z |
. . . . . . . . . . 11
⊢ 0 =
(0g‘𝑅) |
48 | 47 | fvexi 6682 |
. . . . . . . . . 10
⊢ 0 ∈
V |
49 | 48 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 0 ∈ V) |
50 | 44, 45, 46, 49 | suppssr 7884 |
. . . . . . . 8
⊢ ((𝜑 ∧ (1st
‘𝑧) ∈ (𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ))) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) = 0 ) |
51 | 43, 50 | sylan2 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) = 0 ) |
52 | 51 | oveq1d 7179 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = ( 0 · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) |
53 | | evlslem4.r |
. . . . . . 7
⊢ (𝜑 → 𝑅 ∈ Ring) |
54 | 31 | fmpttd 6883 |
. . . . . . . 8
⊢ (𝜑 → (𝑦 ∈ 𝐽 ↦ 𝑌):𝐽⟶𝐵) |
55 | | xp2nd 7740 |
. . . . . . . 8
⊢ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) → (2nd
‘𝑧) ∈ 𝐽) |
56 | | ffvelrn 6853 |
. . . . . . . 8
⊢ (((𝑦 ∈ 𝐽 ↦ 𝑌):𝐽⟶𝐵 ∧ (2nd ‘𝑧) ∈ 𝐽) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) ∈ 𝐵) |
57 | 54, 55, 56 | syl2an 599 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) ∈ 𝐵) |
58 | | evlslem4.b |
. . . . . . . 8
⊢ 𝐵 = (Base‘𝑅) |
59 | | evlslem4.t |
. . . . . . . 8
⊢ · =
(.r‘𝑅) |
60 | 58, 59, 47 | ringlz 19452 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) ∈ 𝐵) → ( 0 · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
61 | 53, 57, 60 | syl2an2r 685 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → ( 0 · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
62 | 52, 61 | eqtrd 2773 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽)) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
63 | | xp2nd 7740 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) → (2nd
‘𝑧) ∈ (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |
64 | | ssidd 3898 |
. . . . . . . . 9
⊢ (𝜑 → ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ) ⊆ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )) |
65 | | evlslem4.j |
. . . . . . . . 9
⊢ (𝜑 → 𝐽 ∈ 𝑊) |
66 | 54, 64, 65, 49 | suppssr 7884 |
. . . . . . . 8
⊢ ((𝜑 ∧ (2nd
‘𝑧) ∈ (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) = 0 ) |
67 | 63, 66 | sylan2 596 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)) = 0 ) |
68 | 67 | oveq2d 7180 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · 0 )) |
69 | | xp1st 7739 |
. . . . . . . 8
⊢ (𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) → (1st
‘𝑧) ∈ 𝐼) |
70 | | ffvelrn 6853 |
. . . . . . . 8
⊢ (((𝑥 ∈ 𝐼 ↦ 𝑋):𝐼⟶𝐵 ∧ (1st ‘𝑧) ∈ 𝐼) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) ∈ 𝐵) |
71 | 44, 69, 70 | syl2an 599 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) ∈ 𝐵) |
72 | 58, 59, 47 | ringrz 19453 |
. . . . . . 7
⊢ ((𝑅 ∈ Ring ∧ ((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) ∈ 𝐵) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · 0 ) = 0 ) |
73 | 53, 71, 72 | syl2an2r 685 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · 0 ) = 0 ) |
74 | 68, 73 | eqtrd 2773 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
75 | 62, 74 | jaodan 957 |
. . . 4
⊢ ((𝜑 ∧ (𝑧 ∈ ((𝐼 ∖ ((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 )) × 𝐽) ∨ 𝑧 ∈ (𝐼 × (𝐽 ∖ ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
76 | 42, 75 | sylan2b 597 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝐼 × 𝐽) ∖ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 )))) → (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧))) = 0 ) |
77 | 46, 65 | xpexd 7486 |
. . 3
⊢ (𝜑 → (𝐼 × 𝐽) ∈ V) |
78 | 76, 77 | suppss2 7888 |
. 2
⊢ (𝜑 → ((𝑧 ∈ (𝐼 × 𝐽) ↦ (((𝑥 ∈ 𝐼 ↦ 𝑋)‘(1st ‘𝑧)) · ((𝑦 ∈ 𝐽 ↦ 𝑌)‘(2nd ‘𝑧)))) supp 0 ) ⊆ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |
79 | 38, 78 | eqsstrd 3913 |
1
⊢ (𝜑 → ((𝑥 ∈ 𝐼, 𝑦 ∈ 𝐽 ↦ (𝑋 · 𝑌)) supp 0 ) ⊆ (((𝑥 ∈ 𝐼 ↦ 𝑋) supp 0 ) × ((𝑦 ∈ 𝐽 ↦ 𝑌) supp 0 ))) |