Metamath Proof Explorer


Theorem uniioombllem5

Description: Lemma for uniioombl . (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses uniioombl.1 φ F : 2
uniioombl.2 φ Disj x . F x
uniioombl.3 S = seq 1 + abs F
uniioombl.a A = ran . F
uniioombl.e φ vol * E
uniioombl.c φ C +
uniioombl.g φ G : 2
uniioombl.s φ E ran . G
uniioombl.t T = seq 1 + abs G
uniioombl.v φ sup ran T * < vol * E + C
uniioombl.m φ M
uniioombl.m2 φ T M sup ran T * < < C
uniioombl.k K = . G 1 M
uniioombl.n φ N
uniioombl.n2 φ j 1 M i = 1 N vol * . F i . G j vol * . G j A < C M
uniioombl.l L = . F 1 N
Assertion uniioombllem5 φ vol * E A + vol * E A vol * E + 4 C

Proof

Step Hyp Ref Expression
1 uniioombl.1 φ F : 2
2 uniioombl.2 φ Disj x . F x
3 uniioombl.3 S = seq 1 + abs F
4 uniioombl.a A = ran . F
5 uniioombl.e φ vol * E
6 uniioombl.c φ C +
7 uniioombl.g φ G : 2
8 uniioombl.s φ E ran . G
9 uniioombl.t T = seq 1 + abs G
10 uniioombl.v φ sup ran T * < vol * E + C
11 uniioombl.m φ M
12 uniioombl.m2 φ T M sup ran T * < < C
13 uniioombl.k K = . G 1 M
14 uniioombl.n φ N
15 uniioombl.n2 φ j 1 M i = 1 N vol * . F i . G j vol * . G j A < C M
16 uniioombl.l L = . F 1 N
17 inss1 E A E
18 7 uniiccdif φ ran . G ran . G vol * ran . G ran . G = 0
19 18 simpld φ ran . G ran . G
20 ovolficcss G : 2 ran . G
21 7 20 syl φ ran . G
22 19 21 sstrd φ ran . G
23 8 22 sstrd φ E
24 ovolsscl E A E E vol * E vol * E A
25 17 23 5 24 mp3an2i φ vol * E A
26 difssd φ E A E
27 ovolsscl E A E E vol * E vol * E A
28 26 23 5 27 syl3anc φ vol * E A
29 25 28 readdcld φ vol * E A + vol * E A
30 inss1 K A K
31 imassrn . G 1 M ran . G
32 31 unissi . G 1 M ran . G
33 13 32 eqsstri K ran . G
34 33 22 sstrid φ K
35 1 2 3 4 5 6 7 8 9 10 uniioombllem1 φ sup ran T * <
36 ssid ran . G ran . G
37 9 ovollb G : 2 ran . G ran . G vol * ran . G sup ran T * <
38 7 36 37 sylancl φ vol * ran . G sup ran T * <
39 ovollecl ran . G sup ran T * < vol * ran . G sup ran T * < vol * ran . G
40 22 35 38 39 syl3anc φ vol * ran . G
41 ovolsscl K ran . G ran . G vol * ran . G vol * K
42 33 22 40 41 mp3an2i φ vol * K
43 ovolsscl K A K K vol * K vol * K A
44 30 34 42 43 mp3an2i φ vol * K A
45 difssd φ K A K
46 ovolsscl K A K K vol * K vol * K A
47 45 34 42 46 syl3anc φ vol * K A
48 44 47 readdcld φ vol * K A + vol * K A
49 6 rpred φ C
50 49 49 readdcld φ C + C
51 48 50 readdcld φ vol * K A + vol * K A + C + C
52 4re 4
53 remulcl 4 C 4 C
54 52 49 53 sylancr φ 4 C
55 5 54 readdcld φ vol * E + 4 C
56 1 2 3 4 5 6 7 8 9 10 11 12 13 uniioombllem3 φ vol * E A + vol * E A < vol * K A + vol * K A + C + C
57 29 51 56 ltled φ vol * E A + vol * E A vol * K A + vol * K A + C + C
58 5 50 readdcld φ vol * E + C + C
59 42 49 readdcld φ vol * K + C
60 inss1 K L K
61 ovolsscl K L K K vol * K vol * K L
62 60 34 42 61 mp3an2i φ vol * K L
63 62 49 readdcld φ vol * K L + C
64 difssd φ K L K
65 ovolsscl K L K K vol * K vol * K L
66 64 34 42 65 syl3anc φ vol * K L
67 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 uniioombllem4 φ vol * K A vol * K L + C
68 imassrn . F 1 N ran . F
69 68 unissi . F 1 N ran . F
70 69 16 4 3sstr4i L A
71 sscon L A K A K L
72 70 71 mp1i φ K A K L
73 64 34 sstrd φ K L
74 ovolss K A K L K L vol * K A vol * K L
75 72 73 74 syl2anc φ vol * K A vol * K L
76 44 47 63 66 67 75 le2addd φ vol * K A + vol * K A vol * K L + C + vol * K L
77 62 recnd φ vol * K L
78 49 recnd φ C
79 66 recnd φ vol * K L
80 77 78 79 add32d φ vol * K L + C + vol * K L = vol * K L + vol * K L + C
81 ioof . : * × * 𝒫
82 inss2 2 2
83 rexpssxrxp 2 * × *
84 82 83 sstri 2 * × *
85 fss F : 2 2 * × * F : * × *
86 1 84 85 sylancl φ F : * × *
87 fco . : * × * 𝒫 F : * × * . F : 𝒫
88 81 86 87 sylancr φ . F : 𝒫
89 ffun . F : 𝒫 Fun . F
90 funiunfv Fun . F n = 1 N . F n = . F 1 N
91 88 89 90 3syl φ n = 1 N . F n = . F 1 N
92 91 16 eqtr4di φ n = 1 N . F n = L
93 fzfid φ 1 N Fin
94 elfznn n 1 N n
95 fvco3 F : 2 n . F n = . F n
96 1 94 95 syl2an φ n 1 N . F n = . F n
97 ffvelrn F : 2 n F n 2
98 1 94 97 syl2an φ n 1 N F n 2
99 98 elin2d φ n 1 N F n 2
100 1st2nd2 F n 2 F n = 1 st F n 2 nd F n
101 99 100 syl φ n 1 N F n = 1 st F n 2 nd F n
102 101 fveq2d φ n 1 N . F n = . 1 st F n 2 nd F n
103 df-ov 1 st F n 2 nd F n = . 1 st F n 2 nd F n
104 102 103 eqtr4di φ n 1 N . F n = 1 st F n 2 nd F n
105 96 104 eqtrd φ n 1 N . F n = 1 st F n 2 nd F n
106 ioombl 1 st F n 2 nd F n dom vol
107 105 106 eqeltrdi φ n 1 N . F n dom vol
108 107 ralrimiva φ n 1 N . F n dom vol
109 finiunmbl 1 N Fin n 1 N . F n dom vol n = 1 N . F n dom vol
110 93 108 109 syl2anc φ n = 1 N . F n dom vol
111 92 110 eqeltrrd φ L dom vol
112 mblsplit L dom vol K vol * K vol * K = vol * K L + vol * K L
113 111 34 42 112 syl3anc φ vol * K = vol * K L + vol * K L
114 113 oveq1d φ vol * K + C = vol * K L + vol * K L + C
115 80 114 eqtr4d φ vol * K L + C + vol * K L = vol * K + C
116 76 115 breqtrd φ vol * K A + vol * K A vol * K + C
117 5 49 readdcld φ vol * E + C
118 9 ovollb G : 2 K ran . G vol * K sup ran T * <
119 7 33 118 sylancl φ vol * K sup ran T * <
120 42 35 117 119 10 letrd φ vol * K vol * E + C
121 42 117 49 120 leadd1dd φ vol * K + C vol * E + C + C
122 5 recnd φ vol * E
123 122 78 78 addassd φ vol * E + C + C = vol * E + C + C
124 121 123 breqtrd φ vol * K + C vol * E + C + C
125 48 59 58 116 124 letrd φ vol * K A + vol * K A vol * E + C + C
126 48 58 50 125 leadd1dd φ vol * K A + vol * K A + C + C vol * E + C + C + C + C
127 50 recnd φ C + C
128 122 127 127 addassd φ vol * E + C + C + C + C = vol * E + C + C + C + C
129 2t2e4 2 2 = 4
130 129 oveq1i 2 2 C = 4 C
131 2cnd φ 2
132 131 131 78 mulassd φ 2 2 C = 2 2 C
133 78 2timesd φ 2 C = C + C
134 133 oveq2d φ 2 2 C = 2 C + C
135 127 2timesd φ 2 C + C = C + C + C + C
136 132 134 135 3eqtrd φ 2 2 C = C + C + C + C
137 130 136 eqtr3id φ 4 C = C + C + C + C
138 137 oveq2d φ vol * E + 4 C = vol * E + C + C + C + C
139 128 138 eqtr4d φ vol * E + C + C + C + C = vol * E + 4 C
140 126 139 breqtrd φ vol * K A + vol * K A + C + C vol * E + 4 C
141 29 51 55 57 140 letrd φ vol * E A + vol * E A vol * E + 4 C