Metamath Proof Explorer


Theorem gsumbagdiagOLD

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

Ref Expression
Hypotheses psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
psrbagconf1o.s 𝑆 = { 𝑦𝐷𝑦r𝐹 }
gsumbagdiagOLD.i ( 𝜑𝐼𝑉 )
gsumbagdiagOLD.f ( 𝜑𝐹𝐷 )
gsumbagdiagOLD.b 𝐵 = ( Base ‘ 𝐺 )
gsumbagdiagOLD.g ( 𝜑𝐺 ∈ CMnd )
gsumbagdiagOLD.x ( ( 𝜑 ∧ ( 𝑗𝑆𝑘 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ) ) → 𝑋𝐵 )
Assertion gsumbagdiagOLD ( 𝜑 → ( 𝐺 Σg ( 𝑗𝑆 , 𝑘 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ↦ 𝑋 ) ) = ( 𝐺 Σg ( 𝑘𝑆 , 𝑗 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑘 ) } ↦ 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 psrbag.d 𝐷 = { 𝑓 ∈ ( ℕ0m 𝐼 ) ∣ ( 𝑓 “ ℕ ) ∈ Fin }
2 psrbagconf1o.s 𝑆 = { 𝑦𝐷𝑦r𝐹 }
3 gsumbagdiagOLD.i ( 𝜑𝐼𝑉 )
4 gsumbagdiagOLD.f ( 𝜑𝐹𝐷 )
5 gsumbagdiagOLD.b 𝐵 = ( Base ‘ 𝐺 )
6 gsumbagdiagOLD.g ( 𝜑𝐺 ∈ CMnd )
7 gsumbagdiagOLD.x ( ( 𝜑 ∧ ( 𝑗𝑆𝑘 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ) ) → 𝑋𝐵 )
8 eqid ( 0g𝐺 ) = ( 0g𝐺 )
9 1 psrbaglefiOLD ( ( 𝐼𝑉𝐹𝐷 ) → { 𝑦𝐷𝑦r𝐹 } ∈ Fin )
10 3 4 9 syl2anc ( 𝜑 → { 𝑦𝐷𝑦r𝐹 } ∈ Fin )
11 2 10 eqeltrid ( 𝜑𝑆 ∈ Fin )
12 ovex ( ℕ0m 𝐼 ) ∈ V
13 1 12 rab2ex { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ∈ V
14 13 a1i ( ( 𝜑𝑗𝑆 ) → { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ∈ V )
15 xpfi ( ( 𝑆 ∈ Fin ∧ 𝑆 ∈ Fin ) → ( 𝑆 × 𝑆 ) ∈ Fin )
16 11 11 15 syl2anc ( 𝜑 → ( 𝑆 × 𝑆 ) ∈ Fin )
17 simprl ( ( 𝜑 ∧ ( 𝑗𝑆𝑘 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ) ) → 𝑗𝑆 )
18 1 2 3 4 gsumbagdiaglemOLD ( ( 𝜑 ∧ ( 𝑗𝑆𝑘 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ) ) → ( 𝑘𝑆𝑗 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑘 ) } ) )
19 18 simpld ( ( 𝜑 ∧ ( 𝑗𝑆𝑘 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ) ) → 𝑘𝑆 )
20 brxp ( 𝑗 ( 𝑆 × 𝑆 ) 𝑘 ↔ ( 𝑗𝑆𝑘𝑆 ) )
21 17 19 20 sylanbrc ( ( 𝜑 ∧ ( 𝑗𝑆𝑘 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ) ) → 𝑗 ( 𝑆 × 𝑆 ) 𝑘 )
22 21 pm2.24d ( ( 𝜑 ∧ ( 𝑗𝑆𝑘 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ) ) → ( ¬ 𝑗 ( 𝑆 × 𝑆 ) 𝑘𝑋 = ( 0g𝐺 ) ) )
23 22 impr ( ( 𝜑 ∧ ( ( 𝑗𝑆𝑘 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ) ∧ ¬ 𝑗 ( 𝑆 × 𝑆 ) 𝑘 ) ) → 𝑋 = ( 0g𝐺 ) )
24 1 2 3 4 gsumbagdiaglemOLD ( ( 𝜑 ∧ ( 𝑘𝑆𝑗 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑘 ) } ) ) → ( 𝑗𝑆𝑘 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ) )
25 18 24 impbida ( 𝜑 → ( ( 𝑗𝑆𝑘 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ) ↔ ( 𝑘𝑆𝑗 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑘 ) } ) ) )
26 5 8 6 11 14 7 16 23 11 25 gsumcom2 ( 𝜑 → ( 𝐺 Σg ( 𝑗𝑆 , 𝑘 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑗 ) } ↦ 𝑋 ) ) = ( 𝐺 Σg ( 𝑘𝑆 , 𝑗 ∈ { 𝑥𝐷𝑥r ≤ ( 𝐹f𝑘 ) } ↦ 𝑋 ) ) )