Metamath Proof Explorer

Theorem gsum2d2lem

Description: Lemma for gsum2d2 : show the function is finitely supported. (Contributed by Mario Carneiro, 28-Dec-2014) (Revised by AV, 9-Jun-2019)

Ref Expression
Hypotheses gsum2d2.b ⊢ 𝐵 = ( Base ‘ 𝐺 )
gsum2d2.z ⊢ 0 = ( 0g ‘ 𝐺 )
gsum2d2.g ⊢ ( 𝜑 → 𝐺 ∈ CMnd )
gsum2d2.a ⊢ ( 𝜑 → 𝐴 ∈ 𝑉 )
gsum2d2.r ⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝐴 ) → 𝐶 ∈ 𝑊 )
gsum2d2.f ⊢ ( ( 𝜑 ∧ ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ) → 𝑋 ∈ 𝐵 )
gsum2d2.u ⊢ ( 𝜑 → 𝑈 ∈ Fin )
gsum2d2.n ⊢ ( ( 𝜑 ∧ ( ( 𝑗 ∈ 𝐴 ∧ 𝑘 ∈ 𝐶 ) ∧ ¬ 𝑗 𝑈 𝑘 ) ) → 𝑋 = 0 )
Assertion gsum2d2lem ( 𝜑 → ( 𝑗 ∈ 𝐴 , 𝑘 ∈ 𝐶 ↦ 𝑋 ) finSupp 0 )

Proof

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 )