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 D = f 0 I | f -1 Fin
psrbagconf1o.s S = y D | y f F
gsumbagdiagOLD.i φ I V
gsumbagdiagOLD.f φ F D
Assertion gsumbagdiaglemOLD φ X S Y x D | x f F f X Y S X x D | x f F f Y

Proof

Step Hyp Ref Expression
1 psrbag.d D = f 0 I | f -1 Fin
2 psrbagconf1o.s S = y D | y f F
3 gsumbagdiagOLD.i φ I V
4 gsumbagdiagOLD.f φ F D
5 simprr φ X S Y x D | x f F f X Y x D | x f F f X
6 breq1 x = Y x f F f X Y f F f X
7 6 elrab Y x D | x f F f X Y D Y f F f X
8 5 7 sylib φ X S Y x D | x f F f X Y D Y f F f X
9 8 simpld φ X S Y x D | x f F f X Y D
10 8 simprd φ X S Y x D | x f F f X Y f F f X
11 3 adantr φ X S Y x D | x f F f X I V
12 4 adantr φ X S Y x D | x f F f X F D
13 simprl φ X S Y x D | x f F f X X S
14 breq1 y = X y f F X f F
15 14 2 elrab2 X S X D X f F
16 13 15 sylib φ X S Y x D | x f F f X X D X f F
17 16 simpld φ X S Y x D | x f F f X X D
18 1 psrbagfOLD I V X D X : I 0
19 11 17 18 syl2anc φ X S Y x D | x f F f X X : I 0
20 16 simprd φ X S Y x D | x f F f X X f F
21 1 psrbagconOLD I V F D X : I 0 X f F F f X D F f X f F
22 11 12 19 20 21 syl13anc φ X S Y x D | x f F f X F f X D F f X f F
23 22 simprd φ X S Y x D | x f F f X F f X f F
24 1 psrbagfOLD I V Y D Y : I 0
25 11 9 24 syl2anc φ X S Y x D | x f F f X Y : I 0
26 22 simpld φ X S Y x D | x f F f X F f X D
27 1 psrbagfOLD I V F f X D F f X : I 0
28 11 26 27 syl2anc φ X S Y x D | x f F f X F f X : I 0
29 1 psrbagfOLD I V F D F : I 0
30 11 12 29 syl2anc φ X S Y x D | x f F f X F : I 0
31 nn0re u 0 u
32 nn0re v 0 v
33 nn0re w 0 w
34 letr u v w u v v w u w
35 31 32 33 34 syl3an u 0 v 0 w 0 u v v w u w
36 35 adantl φ X S Y x D | x f F f X u 0 v 0 w 0 u v v w u w
37 11 25 28 30 36 caoftrn φ X S Y x D | x f F f X Y f F f X F f X f F Y f F
38 10 23 37 mp2and φ X S Y x D | x f F f X Y f F
39 breq1 y = Y y f F Y f F
40 39 2 elrab2 Y S Y D Y f F
41 9 38 40 sylanbrc φ X S Y x D | x f F f X Y S
42 breq1 x = X x f F f Y X f F f Y
43 19 ffvelrnda φ X S Y x D | x f F f X z I X z 0
44 25 ffvelrnda φ X S Y x D | x f F f X z I Y z 0
45 30 ffvelrnda φ X S Y x D | x f F f X z I F z 0
46 nn0re X z 0 X z
47 nn0re Y z 0 Y z
48 nn0re F z 0 F z
49 leaddsub2 X z Y z F z X z + Y z F z Y z F z X z
50 leaddsub X z Y z F z X z + Y z F z X z F z Y z
51 49 50 bitr3d X z Y z F z Y z F z X z X z F z Y z
52 46 47 48 51 syl3an X z 0 Y z 0 F z 0 Y z F z X z X z F z Y z
53 43 44 45 52 syl3anc φ X S Y x D | x f F f X z I Y z F z X z X z F z Y z
54 53 ralbidva φ X S Y x D | x f F f X z I Y z F z X z z I X z F z Y z
55 ovexd φ X S Y x D | x f F f X z I F z X z V
56 25 feqmptd φ X S Y x D | x f F f X Y = z I Y z
57 30 ffnd φ X S Y x D | x f F f X F Fn I
58 19 ffnd φ X S Y x D | x f F f X X Fn I
59 inidm I I = I
60 eqidd φ X S Y x D | x f F f X z I F z = F z
61 eqidd φ X S Y x D | x f F f X z I X z = X z
62 57 58 11 11 59 60 61 offval φ X S Y x D | x f F f X F f X = z I F z X z
63 11 44 55 56 62 ofrfval2 φ X S Y x D | x f F f X Y f F f X z I Y z F z X z
64 ovexd φ X S Y x D | x f F f X z I F z Y z V
65 19 feqmptd φ X S Y x D | x f F f X X = z I X z
66 25 ffnd φ X S Y x D | x f F f X Y Fn I
67 eqidd φ X S Y x D | x f F f X z I Y z = Y z
68 57 66 11 11 59 60 67 offval φ X S Y x D | x f F f X F f Y = z I F z Y z
69 11 43 64 65 68 ofrfval2 φ X S Y x D | x f F f X X f F f Y z I X z F z Y z
70 54 63 69 3bitr4d φ X S Y x D | x f F f X Y f F f X X f F f Y
71 10 70 mpbid φ X S Y x D | x f F f X X f F f Y
72 42 17 71 elrabd φ X S Y x D | x f F f X X x D | x f F f Y
73 41 72 jca φ X S Y x D | x f F f X Y S X x D | x f F f Y