Theorem osumlem4 5533

Description: Lemma for osum 5538.

Hypotheses

Ref	Expression
osumlem4.1	|- A e. CH
osumlem4.2	|- B e. CH
osumlem4.3	|- B (_ (_|_` A)
osumlem4.4	|- G e. V
osumlem4.5	|- H e. V

Assertion

Ref	Expression
osumlem4	|- ((((F:NN-->A /\ G:NN-->B) /\ A.w e. NN (H` w) = ((F` w) +v (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (H ~~>v z -> G ~~>v y))

Distinct variable group(s):   w,A   w,B   w,F   w,G   w,H   x,w   y,w   z,w

Proof of Theorem osumlem4

Step	Hyp	Ref	Expression
1		osumlem4.2	. . . . . . . 8 |- B e. CH
2	1	chssi 5136	. . . . . . 7 |- B (_ H~
3		fss 2759	. . . . . . 7 |- ((G:NN-->B /\ B (_ H~) -> G:NN-->H~)
4	2, 3	mpan2 519	. . . . . 6 |- (G:NN-->B -> G:NN-->H~)
5	4	ad2antlr 321	. . . . 5 |- (((F:NN-->A /\ G:NN-->B) /\ A.w e. NN (H` w) = ((F` w) +v (G` w))) -> G:NN-->H~)
6		osumlem4.1	. . . . . . . . 9 |- A e. CH
7	6	chshi 5132	. . . . . . . 8 |- A e. SH
8		shocss 5167	. . . . . . . 8 |- (A e. SH -> (_|_` A) (_ H~)
9	7, 8	ax-mp 6	. . . . . . 7 |- (_|_` A) (_ H~
10	9	sseli 1504	. . . . . 6 |- (y e. (_|_` A) -> y e. H~)
11	10	ad2antlr 321	. . . . 5 |- (((x e. A /\ y e. (_|_` A)) /\ z = (x +v y)) -> y e. H~)
12	5, 11	anim12i 268	. . . 4 |- ((((F:NN-->A /\ G:NN-->B) /\ A.w e. NN (H` w) = ((F` w) +v (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (G:NN-->H~ /\ y e. H~))
13	12	a1d 14	. . 3 |- ((((F:NN-->A /\ G:NN-->B) /\ A.w e. NN (H` w) = ((F` w) +v (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (H ~~>v z -> (G:NN-->H~ /\ y e. H~)))
14		ffvrn 2890	. . . . . . . . . . . . . . . . . . 19 |- ((F:NN-->A /\ w e. NN) -> (F` w) e. A)
15	14	exp 291	. . . . . . . . . . . . . . . . . 18 |- (F:NN-->A -> (w e. NN -> (F` w) e. A))
16	15	com12 13	. . . . . . . . . . . . . . . . 17 |- (w e. NN -> (F:NN-->A -> (F` w) e. A))
17		ffvrn 2890	. . . . . . . . . . . . . . . . . . 19 |- ((G:NN-->B /\ w e. NN) -> (G` w) e. B)
18	17	exp 291	. . . . . . . . . . . . . . . . . 18 |- (G:NN-->B -> (w e. NN -> (G` w) e. B))
19	18	com12 13	. . . . . . . . . . . . . . . . 17 |- (w e. NN -> (G:NN-->B -> (G` w) e. B))
20	16, 19	anim12d 431	. . . . . . . . . . . . . . . 16 |- (w e. NN -> ((F:NN-->A /\ G:NN-->B) -> ((F` w) e. A /\ (G` w) e. B)))
21		osumlem4.3	. . . . . . . . . . . . . . . . . . . . 21 |- B (_ (_|_` A)
22		pm4.2 148	. . . . . . . . . . . . . . . . . . . . 21 |- (((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +v (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) <-> ((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +v (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))))
23	6, 1, 21, 22	osumlem3 5532	. . . . . . . . . . . . . . . . . . . 20 |- (((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +v (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (norm` ((G` w) -v y)) <_ (norm` ((H` w) -v z)))
24	23	adantr 306	. . . . . . . . . . . . . . . . . . 19 |- ((((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +v (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) /\ u e. RR) -> (norm` ((G` w) -v y)) <_ (norm` ((H` w) -v z)))
25	6, 1, 21, 22	osumlem1 5530	. . . . . . . . . . . . . . . . . . . . 21 |- (((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +v (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> ((((F` w) e. H~ /\ (G` w) e. H~) /\ (H` w) e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)))
26		lelttrt 4289	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((norm` ((G` w) -v y)) e. RR /\ (norm` ((H` w) -v z)) e. RR /\ u e. RR) -> (((norm` ((G` w) -v y)) <_ (norm` ((H` w) -v z)) /\ (norm` ((H` w) -v z)) < u) -> (norm` ((G` w) -v y)) < u))
27	26	3exp 611	. . . . . . . . . . . . . . . . . . . . . 22 |- ((norm` ((G` w) -v y)) e. RR -> ((norm` ((H` w) -v z)) e. RR -> (u e. RR -> (((norm` ((G` w) -v y)) <_ (norm` ((H` w) -v z)) /\ (norm` ((H` w) -v z)) < u) -> (norm` ((G` w) -v y)) < u))))
28		hvsubclt 4998	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((G` w) e. H~ /\ y e. H~) -> ((G` w) -v y) e. H~)
29		normclt 5076	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (((G` w) -v y) e. H~ -> (norm` ((G` w) -v y)) e. RR)
30	28, 29	syl 12	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((G` w) e. H~ /\ y e. H~) -> (norm` ((G` w) -v y)) e. RR)
31	30	adantrl 311	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((G` w) e. H~ /\ (x e. H~ /\ y e. H~)) -> (norm` ((G` w) -v y)) e. RR)
32	31	adantll 309	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((F` w) e. H~ /\ (G` w) e. H~) /\ (x e. H~ /\ y e. H~)) -> (norm` ((G` w) -v y)) e. RR)
33	32	adantrr 312	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((F` w) e. H~ /\ (G` w) e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (norm` ((G` w) -v y)) e. RR)
34	33	adantlr 310	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((F` w) e. H~ /\ (G` w) e. H~) /\ (H` w) e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (norm` ((G` w) -v y)) e. RR)
35		hvsubclt 4998	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((H` w) e. H~ /\ z e. H~) -> ((H` w) -v z) e. H~)
36		normclt 5076	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((H` w) -v z) e. H~ -> (norm` ((H` w) -v z)) e. RR)
37	35, 36	syl 12	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((H` w) e. H~ /\ z e. H~) -> (norm` ((H` w) -v z)) e. RR)
38	37	adantrl 311	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((H` w) e. H~ /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (norm` ((H` w) -v z)) e. RR)
39	38	adantll 309	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((F` w) e. H~ /\ (G` w) e. H~) /\ (H` w) e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (norm` ((H` w) -v z)) e. RR)
40	27, 34, 39	sylc 62	. . . . . . . . . . . . . . . . . . . . 21 |- (((((F` w) e. H~ /\ (G` w) e. H~) /\ (H` w) e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (u e. RR -> (((norm` ((G` w) -v y)) <_ (norm` ((H` w) -v z)) /\ (norm` ((H` w) -v z)) < u) -> (norm` ((G` w) -v y)) < u)))
41	25, 40	syl 12	. . . . . . . . . . . . . . . . . . . 20 |- (((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +v (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) -> (u e. RR -> (((norm` ((G` w) -v y)) <_ (norm` ((H` w) -v z)) /\ (norm` ((H` w) -v z)) < u) -> (norm` ((G` w) -v y)) < u)))
42	41	imp 277	. . . . . . . . . . . . . . . . . . 19 |- ((((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +v (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +v y))) /\ u e. RR) -> (((norm` ((G