Metamath Proof Explorer


Theorem gsumbagdiaglem

Description: Lemma for gsumbagdiag . (Contributed by Mario Carneiro, 5-Jan-2015) Remove a sethood hypothesis. (Revised by SN, 6-Aug-2024)

Ref Expression
Hypotheses gsumbagdiag.d D = f 0 I | f -1 Fin
gsumbagdiag.s S = y D | y f F
gsumbagdiag.f φ F D
Assertion gsumbagdiaglem φ 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 gsumbagdiag.d D = f 0 I | f -1 Fin
2 gsumbagdiag.s S = y D | y f F
3 gsumbagdiag.f φ F D
4 simprr φ X S Y x D | x f F f X Y x D | x f F f X
5 breq1 x = Y x f F f X Y f F f X
6 5 elrab Y x D | x f F f X Y D Y f F f X
7 4 6 sylib φ X S Y x D | x f F f X Y D Y f F f X
8 7 simpld φ X S Y x D | x f F f X Y D
9 7 simprd φ X S Y x D | x f F f X Y f F f X
10 3 adantr φ X S Y x D | x f F f X F D
11 simprl φ X S Y x D | x f F f X X S
12 breq1 y = X y f F X f F
13 12 2 elrab2 X S X D X f F
14 11 13 sylib φ X S Y x D | x f F f X X D X f F
15 14 simpld φ X S Y x D | x f F f X X D
16 1 psrbagf X D X : I 0
17 15 16 syl φ X S Y x D | x f F f X X : I 0
18 14 simprd φ X S Y x D | x f F f X X f F
19 1 psrbagcon F D X : I 0 X f F F f X D F f X f F
20 10 17 18 19 syl3anc φ X S Y x D | x f F f X F f X D F f X f F
21 20 simprd φ X S Y x D | x f F f X F f X f F
22 1 psrbagf F D F : I 0
23 10 22 syl φ X S Y x D | x f F f X F : I 0
24 23 ffnd φ X S Y x D | x f F f X F Fn I
25 10 24 fndmexd φ X S Y x D | x f F f X I V
26 1 psrbagf Y D Y : I 0
27 8 26 syl φ X S Y x D | x f F f X Y : I 0
28 20 simpld φ X S Y x D | x f F f X F f X D
29 1 psrbagf F f X D F f X : I 0
30 28 29 syl φ X S Y x D | x f F f X F f X : 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 25 27 30 23 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 9 21 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 8 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 17 ffvelrnda φ X S Y x D | x f F f X z I X z 0
44 27 ffvelrnda φ X S Y x D | x f F f X z I Y z 0
45 23 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 27 feqmptd φ X S Y x D | x f F f X Y = z I Y z
57 17 ffnd φ X S Y x D | x f F f X X Fn I
58 inidm I I = I
59 eqidd φ X S Y x D | x f F f X z I F z = F z
60 eqidd φ X S Y x D | x f F f X z I X z = X z
61 24 57 25 25 58 59 60 offval φ X S Y x D | x f F f X F f X = z I F z X z
62 25 44 55 56 61 ofrfval2 φ X S Y x D | x f F f X Y f F f X z I Y z F z X z
63 ovexd φ X S Y x D | x f F f X z I F z Y z V
64 17 feqmptd φ X S Y x D | x f F f X X = z I X z
65 27 ffnd φ X S Y x D | x f F f X Y Fn I
66 eqidd φ X S Y x D | x f F f X z I Y z = Y z
67 24 65 25 25 58 59 66 offval φ X S Y x D | x f F f X F f Y = z I F z Y z
68 25 43 63 64 67 ofrfval2 φ X S Y x D | x f F f X X f F f Y z I X z F z Y z
69 54 62 68 3bitr4d φ X S Y x D | x f F f X Y f F f X X f F f Y
70 9 69 mpbid φ X S Y x D | x f F f X X f F f Y
71 42 15 70 elrabd φ X S Y x D | x f F f X X x D | x f F f Y
72 41 71 jca φ X S Y x D | x f F f X Y S X x D | x f F f Y