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 )