Step |
Hyp |
Ref |
Expression |
1 |
|
gsum2d2.b |
⊢ 𝐵 = ( Base ‘ 𝐺 ) |
2 |
|
gsum2d2.z |
⊢ 0 = ( 0g ‘ 𝐺 ) |
3 |
|
gsum2d2.g |
⊢ ( 𝜑 → 𝐺 ∈ CMnd ) |
4 |
|
gsum2d2.a |
⊢ ( 𝜑 → 𝐴 ∈ 𝑉 ) |
5 |
|
gsum2d2.r |
⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑊 ) |
6 |
|
gsum2d2.f |
⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) → 𝑋 ∈ 𝐵 ) |
7 |
|
gsum2d2.u |
⊢ ( 𝜑 → 𝑈 ∈ Fin ) |
8 |
|
gsum2d2.n |
⊢ ( ( 𝜑 ∧ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ∧ ¬ 𝑗 𝑈 𝑘 ) ) → 𝑋 = 0 ) |
9 |
|
eqid |
⊢ ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) = ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) |
10 |
9
|
mpofun |
⊢ Fun ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) |
11 |
10
|
a1i |
⊢ ( 𝜑 → Fun ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ) |
12 |
6
|
ralrimivva |
⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐶 𝑋 ∈ 𝐵 ) |
13 |
9
|
fmpox |
⊢ ( ∀ 𝑗 ∈ 𝐴 ∀ 𝑘 ∈ 𝐶 𝑋 ∈ 𝐵 ↔ ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) : ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ⟶ 𝐵 ) |
14 |
12 13
|
sylib |
⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) : ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ⟶ 𝐵 ) |
15 |
|
nfv |
⊢ Ⅎ 𝑗 𝜑 |
16 |
|
nfiu1 |
⊢ Ⅎ 𝑗 ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) |
17 |
|
nfcv |
⊢ Ⅎ 𝑗 𝑈 |
18 |
16 17
|
nfdif |
⊢ Ⅎ 𝑗 ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) |
19 |
18
|
nfcri |
⊢ Ⅎ 𝑗 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) |
20 |
15 19
|
nfan |
⊢ Ⅎ 𝑗 ( 𝜑 ∧ 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ) |
21 |
|
nfmpo1 |
⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) |
22 |
|
nfcv |
⊢ Ⅎ 𝑗 𝑧 |
23 |
21 22
|
nffv |
⊢ Ⅎ 𝑗 ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 𝑧 ) |
24 |
23
|
nfeq1 |
⊢ Ⅎ 𝑗 ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 𝑧 ) = 0 |
25 |
|
relxp |
⊢ Rel ( { 𝑗 } × 𝐶 ) |
26 |
25
|
rgenw |
⊢ ∀ 𝑗 ∈ 𝐴 Rel ( { 𝑗 } × 𝐶 ) |
27 |
|
reliun |
⊢ ( Rel ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ ∀ 𝑗 ∈ 𝐴 Rel ( { 𝑗 } × 𝐶 ) ) |
28 |
26 27
|
mpbir |
⊢ Rel ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) |
29 |
|
eldifi |
⊢ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ) |
30 |
29
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ) → 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ) |
31 |
|
elrel |
⊢ ( ( Rel ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∧ 𝑧 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ) → ∃ 𝑗 ∃ 𝑘 𝑧 = 〈 𝑗 , 𝑘 〉 ) |
32 |
28 30 31
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ) → ∃ 𝑗 ∃ 𝑘 𝑧 = 〈 𝑗 , 𝑘 〉 ) |
33 |
|
nfv |
⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ) |
34 |
|
nfmpo2 |
⊢ Ⅎ 𝑘 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) |
35 |
|
nfcv |
⊢ Ⅎ 𝑘 𝑧 |
36 |
34 35
|
nffv |
⊢ Ⅎ 𝑘 ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 𝑧 ) |
37 |
36
|
nfeq1 |
⊢ Ⅎ 𝑘 ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 𝑧 ) = 0 |
38 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → 𝑧 = 〈 𝑗 , 𝑘 〉 ) |
39 |
38
|
fveq2d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 𝑧 ) = ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 〈 𝑗 , 𝑘 〉 ) ) |
40 |
|
df-ov |
⊢ ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) = ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 〈 𝑗 , 𝑘 〉 ) |
41 |
|
simprl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ) |
42 |
38 41
|
eqeltrrd |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → 〈 𝑗 , 𝑘 〉 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ) |
43 |
42
|
eldifad |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → 〈 𝑗 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ) |
44 |
|
opeliunxp |
⊢ ( 〈 𝑗 , 𝑘 〉 ∈ ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ↔ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) |
45 |
43 44
|
sylib |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) |
46 |
45
|
simpld |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → 𝑗 ∈ 𝐴 ) |
47 |
45
|
simprd |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → 𝑘 ∈ 𝐶 ) |
48 |
45 6
|
syldan |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → 𝑋 ∈ 𝐵 ) |
49 |
9
|
ovmpt4g |
⊢ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵 ) → ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) = 𝑋 ) |
50 |
46 47 48 49
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → ( 𝑗 ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) 𝑘 ) = 𝑋 ) |
51 |
40 50
|
eqtr3id |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 〈 𝑗 , 𝑘 〉 ) = 𝑋 ) |
52 |
|
eldifn |
⊢ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) → ¬ 𝑧 ∈ 𝑈 ) |
53 |
52
|
ad2antrl |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → ¬ 𝑧 ∈ 𝑈 ) |
54 |
38
|
eleq1d |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → ( 𝑧 ∈ 𝑈 ↔ 〈 𝑗 , 𝑘 〉 ∈ 𝑈 ) ) |
55 |
|
df-br |
⊢ ( 𝑗 𝑈 𝑘 ↔ 〈 𝑗 , 𝑘 〉 ∈ 𝑈 ) |
56 |
54 55
|
bitr4di |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → ( 𝑧 ∈ 𝑈 ↔ 𝑗 𝑈 𝑘 ) ) |
57 |
53 56
|
mtbid |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → ¬ 𝑗 𝑈 𝑘 ) |
58 |
45 57
|
jca |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ∧ ¬ 𝑗 𝑈 𝑘 ) ) |
59 |
58 8
|
syldan |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → 𝑋 = 0 ) |
60 |
39 51 59
|
3eqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ∧ 𝑧 = 〈 𝑗 , 𝑘 〉 ) ) → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 𝑧 ) = 0 ) |
61 |
60
|
expr |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ) → ( 𝑧 = 〈 𝑗 , 𝑘 〉 → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 𝑧 ) = 0 ) ) |
62 |
33 37 61
|
exlimd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ) → ( ∃ 𝑘 𝑧 = 〈 𝑗 , 𝑘 〉 → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 𝑧 ) = 0 ) ) |
63 |
20 24 32 62
|
exlimimdd |
⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( ∪ 𝑗 ∈ 𝐴 ( { 𝑗 } × 𝐶 ) ∖ 𝑈 ) ) → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ‘ 𝑧 ) = 0 ) |
64 |
14 63
|
suppss |
⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) supp 0 ) ⊆ 𝑈 ) |
65 |
7 64
|
ssfid |
⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) supp 0 ) ∈ Fin ) |
66 |
5
|
ralrimiva |
⊢ ( 𝜑 → ∀ 𝑗 ∈ 𝐴 𝐶 ∈ 𝑊 ) |
67 |
9
|
mpoexxg |
⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑗 ∈ 𝐴 𝐶 ∈ 𝑊 ) → ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ∈ V ) |
68 |
4 66 67
|
syl2anc |
⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ∈ V ) |
69 |
2
|
fvexi |
⊢ 0 ∈ V |
70 |
69
|
a1i |
⊢ ( 𝜑 → 0 ∈ V ) |
71 |
|
isfsupp |
⊢ ( ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ∈ V ∧ 0 ∈ V ) → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) finSupp 0 ↔ ( Fun ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ∧ ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) supp 0 ) ∈ Fin ) ) ) |
72 |
68 70 71
|
syl2anc |
⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) finSupp 0 ↔ ( Fun ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) ∧ ( ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) supp 0 ) ∈ Fin ) ) ) |
73 |
11 65 72
|
mpbir2and |
⊢ ( 𝜑 → ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) finSupp 0 ) |