Metamath Proof Explorer


Theorem gsumbagdiaglemOLD

Description: Obsolete version of gsumbagdiaglem as of 6-Aug-2024. (Contributed by Mario Carneiro, 5-Jan-2015) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
psrbagconf1o.s 𝑆 = { 𝑦𝐷𝑦r𝐹 }
gsumbagdiagOLD.i ( 𝜑𝐼𝑉 )
gsumbagdiagOLD.f ( 𝜑𝐹𝐷 )
Assertion gsumbagdiaglemOLD ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( 𝑌𝑆𝑋 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑌 ) } ) )

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 psrbagconf1o.s 𝑆 = { 𝑦𝐷𝑦r𝐹 }
3 gsumbagdiagOLD.i ( 𝜑𝐼𝑉 )
4 gsumbagdiagOLD.f ( 𝜑𝐹𝐷 )
5 simprr ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } )
6 breq1 ( 𝑥 = 𝑌 → ( 𝑥r ≤ ( 𝐹f𝑋 ) ↔ 𝑌r ≤ ( 𝐹f𝑋 ) ) )
7 6 elrab ( 𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ↔ ( 𝑌𝐷𝑌r ≤ ( 𝐹f𝑋 ) ) )
8 5 7 sylib ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( 𝑌𝐷𝑌r ≤ ( 𝐹f𝑋 ) ) )
9 8 simpld ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑌𝐷 )
10 8 simprd ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑌r ≤ ( 𝐹f𝑋 ) )
11 3 adantr ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝐼𝑉 )
12 4 adantr ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝐹𝐷 )
13 simprl ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑋𝑆 )
14 breq1 ( 𝑦 = 𝑋 → ( 𝑦r𝐹𝑋r𝐹 ) )
15 14 2 elrab2 ( 𝑋𝑆 ↔ ( 𝑋𝐷𝑋r𝐹 ) )
16 13 15 sylib ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( 𝑋𝐷𝑋r𝐹 ) )
17 16 simpld ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑋𝐷 )
18 1 psrbagfOLD ( ( 𝐼𝑉𝑋𝐷 ) → 𝑋 : 𝐼 ⟶ ℕ0 )
19 11 17 18 syl2anc ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑋 : 𝐼 ⟶ ℕ0 )
20 16 simprd ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑋r𝐹 )
21 1 psrbagconOLD ( ( 𝐼𝑉 ∧ ( 𝐹𝐷𝑋 : 𝐼 ⟶ ℕ0𝑋r𝐹 ) ) → ( ( 𝐹f𝑋 ) ∈ 𝐷 ∧ ( 𝐹f𝑋 ) ∘r𝐹 ) )
22 11 12 19 20 21 syl13anc ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( ( 𝐹f𝑋 ) ∈ 𝐷 ∧ ( 𝐹f𝑋 ) ∘r𝐹 ) )
23 22 simprd ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( 𝐹f𝑋 ) ∘r𝐹 )
24 1 psrbagfOLD ( ( 𝐼𝑉𝑌𝐷 ) → 𝑌 : 𝐼 ⟶ ℕ0 )
25 11 9 24 syl2anc ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑌 : 𝐼 ⟶ ℕ0 )
26 22 simpld ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( 𝐹f𝑋 ) ∈ 𝐷 )
27 1 psrbagfOLD ( ( 𝐼𝑉 ∧ ( 𝐹f𝑋 ) ∈ 𝐷 ) → ( 𝐹f𝑋 ) : 𝐼 ⟶ ℕ0 )
28 11 26 27 syl2anc ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( 𝐹f𝑋 ) : 𝐼 ⟶ ℕ0 )
29 1 psrbagfOLD ( ( 𝐼𝑉𝐹𝐷 ) → 𝐹 : 𝐼 ⟶ ℕ0 )
30 11 12 29 syl2anc ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝐹 : 𝐼 ⟶ ℕ0 )
31 nn0re ( 𝑢 ∈ ℕ0𝑢 ∈ ℝ )
32 nn0re ( 𝑣 ∈ ℕ0𝑣 ∈ ℝ )
33 nn0re ( 𝑤 ∈ ℕ0𝑤 ∈ ℝ )
34 letr ( ( 𝑢 ∈ ℝ ∧ 𝑣 ∈ ℝ ∧ 𝑤 ∈ ℝ ) → ( ( 𝑢𝑣𝑣𝑤 ) → 𝑢𝑤 ) )
35 31 32 33 34 syl3an ( ( 𝑢 ∈ ℕ0𝑣 ∈ ℕ0𝑤 ∈ ℕ0 ) → ( ( 𝑢𝑣𝑣𝑤 ) → 𝑢𝑤 ) )
36 35 adantl ( ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) ∧ ( 𝑢 ∈ ℕ0𝑣 ∈ ℕ0𝑤 ∈ ℕ0 ) ) → ( ( 𝑢𝑣𝑣𝑤 ) → 𝑢𝑤 ) )
37 11 25 28 30 36 caoftrn ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( ( 𝑌r ≤ ( 𝐹f𝑋 ) ∧ ( 𝐹f𝑋 ) ∘r𝐹 ) → 𝑌r𝐹 ) )
38 10 23 37 mp2and ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑌r𝐹 )
39 breq1 ( 𝑦 = 𝑌 → ( 𝑦r𝐹𝑌r𝐹 ) )
40 39 2 elrab2 ( 𝑌𝑆 ↔ ( 𝑌𝐷𝑌r𝐹 ) )
41 9 38 40 sylanbrc ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑌𝑆 )
42 breq1 ( 𝑥 = 𝑋 → ( 𝑥r ≤ ( 𝐹f𝑌 ) ↔ 𝑋r ≤ ( 𝐹f𝑌 ) ) )
43 19 ffvelrnda ( ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) ∧ 𝑧𝐼 ) → ( 𝑋𝑧 ) ∈ ℕ0 )
44 25 ffvelrnda ( ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) ∧ 𝑧𝐼 ) → ( 𝑌𝑧 ) ∈ ℕ0 )
45 30 ffvelrnda ( ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) ∧ 𝑧𝐼 ) → ( 𝐹𝑧 ) ∈ ℕ0 )
46 nn0re ( ( 𝑋𝑧 ) ∈ ℕ0 → ( 𝑋𝑧 ) ∈ ℝ )
47 nn0re ( ( 𝑌𝑧 ) ∈ ℕ0 → ( 𝑌𝑧 ) ∈ ℝ )
48 nn0re ( ( 𝐹𝑧 ) ∈ ℕ0 → ( 𝐹𝑧 ) ∈ ℝ )
49 leaddsub2 ( ( ( 𝑋𝑧 ) ∈ ℝ ∧ ( 𝑌𝑧 ) ∈ ℝ ∧ ( 𝐹𝑧 ) ∈ ℝ ) → ( ( ( 𝑋𝑧 ) + ( 𝑌𝑧 ) ) ≤ ( 𝐹𝑧 ) ↔ ( 𝑌𝑧 ) ≤ ( ( 𝐹𝑧 ) − ( 𝑋𝑧 ) ) ) )
50 leaddsub ( ( ( 𝑋𝑧 ) ∈ ℝ ∧ ( 𝑌𝑧 ) ∈ ℝ ∧ ( 𝐹𝑧 ) ∈ ℝ ) → ( ( ( 𝑋𝑧 ) + ( 𝑌𝑧 ) ) ≤ ( 𝐹𝑧 ) ↔ ( 𝑋𝑧 ) ≤ ( ( 𝐹𝑧 ) − ( 𝑌𝑧 ) ) ) )
51 49 50 bitr3d ( ( ( 𝑋𝑧 ) ∈ ℝ ∧ ( 𝑌𝑧 ) ∈ ℝ ∧ ( 𝐹𝑧 ) ∈ ℝ ) → ( ( 𝑌𝑧 ) ≤ ( ( 𝐹𝑧 ) − ( 𝑋𝑧 ) ) ↔ ( 𝑋𝑧 ) ≤ ( ( 𝐹𝑧 ) − ( 𝑌𝑧 ) ) ) )
52 46 47 48 51 syl3an ( ( ( 𝑋𝑧 ) ∈ ℕ0 ∧ ( 𝑌𝑧 ) ∈ ℕ0 ∧ ( 𝐹𝑧 ) ∈ ℕ0 ) → ( ( 𝑌𝑧 ) ≤ ( ( 𝐹𝑧 ) − ( 𝑋𝑧 ) ) ↔ ( 𝑋𝑧 ) ≤ ( ( 𝐹𝑧 ) − ( 𝑌𝑧 ) ) ) )
53 43 44 45 52 syl3anc ( ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) ∧ 𝑧𝐼 ) → ( ( 𝑌𝑧 ) ≤ ( ( 𝐹𝑧 ) − ( 𝑋𝑧 ) ) ↔ ( 𝑋𝑧 ) ≤ ( ( 𝐹𝑧 ) − ( 𝑌𝑧 ) ) ) )
54 53 ralbidva ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( ∀ 𝑧𝐼 ( 𝑌𝑧 ) ≤ ( ( 𝐹𝑧 ) − ( 𝑋𝑧 ) ) ↔ ∀ 𝑧𝐼 ( 𝑋𝑧 ) ≤ ( ( 𝐹𝑧 ) − ( 𝑌𝑧 ) ) ) )
55 ovexd ( ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) ∧ 𝑧𝐼 ) → ( ( 𝐹𝑧 ) − ( 𝑋𝑧 ) ) ∈ V )
56 25 feqmptd ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑌 = ( 𝑧𝐼 ↦ ( 𝑌𝑧 ) ) )
57 30 ffnd ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝐹 Fn 𝐼 )
58 19 ffnd ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑋 Fn 𝐼 )
59 inidm ( 𝐼𝐼 ) = 𝐼
60 eqidd ( ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) ∧ 𝑧𝐼 ) → ( 𝐹𝑧 ) = ( 𝐹𝑧 ) )
61 eqidd ( ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) ∧ 𝑧𝐼 ) → ( 𝑋𝑧 ) = ( 𝑋𝑧 ) )
62 57 58 11 11 59 60 61 offval ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( 𝐹f𝑋 ) = ( 𝑧𝐼 ↦ ( ( 𝐹𝑧 ) − ( 𝑋𝑧 ) ) ) )
63 11 44 55 56 62 ofrfval2 ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( 𝑌r ≤ ( 𝐹f𝑋 ) ↔ ∀ 𝑧𝐼 ( 𝑌𝑧 ) ≤ ( ( 𝐹𝑧 ) − ( 𝑋𝑧 ) ) ) )
64 ovexd ( ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) ∧ 𝑧𝐼 ) → ( ( 𝐹𝑧 ) − ( 𝑌𝑧 ) ) ∈ V )
65 19 feqmptd ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑋 = ( 𝑧𝐼 ↦ ( 𝑋𝑧 ) ) )
66 25 ffnd ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑌 Fn 𝐼 )
67 eqidd ( ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) ∧ 𝑧𝐼 ) → ( 𝑌𝑧 ) = ( 𝑌𝑧 ) )
68 57 66 11 11 59 60 67 offval ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( 𝐹f𝑌 ) = ( 𝑧𝐼 ↦ ( ( 𝐹𝑧 ) − ( 𝑌𝑧 ) ) ) )
69 11 43 64 65 68 ofrfval2 ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( 𝑋r ≤ ( 𝐹f𝑌 ) ↔ ∀ 𝑧𝐼 ( 𝑋𝑧 ) ≤ ( ( 𝐹𝑧 ) − ( 𝑌𝑧 ) ) ) )
70 54 63 69 3bitr4d ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( 𝑌r ≤ ( 𝐹f𝑋 ) ↔ 𝑋r ≤ ( 𝐹f𝑌 ) ) )
71 10 70 mpbid ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑋r ≤ ( 𝐹f𝑌 ) )
72 42 17 71 elrabd ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → 𝑋 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑌 ) } )
73 41 72 jca ( ( 𝜑 ∧ ( 𝑋𝑆𝑌 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑋 ) } ) ) → ( 𝑌𝑆𝑋 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑌 ) } ) )