Theorem osumlem4 9581

Description: Lemma for osum 9586.

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) +h (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) -> (H ~~>v z -> G ~~>v y))

Distinct variable groups:   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		ffvelrn 3814	. . . . . . . . . . . . . . . . . 18 |- ((F:NN-->A /\ w e. NN) -> (F` w) e. A)
2	1	expcom 374	. . . . . . . . . . . . . . . . 17 |- (w e. NN -> (F:NN-->A -> (F` w) e. A))
3		ffvelrn 3814	. . . . . . . . . . . . . . . . . 18 |- ((G:NN-->B /\ w e. NN) -> (G` w) e. B)
4	3	expcom 374	. . . . . . . . . . . . . . . . 17 |- (w e. NN -> (G:NN-->B -> (G` w) e. B))
5	2, 4	anim12d 558	. . . . . . . . . . . . . . . 16 |- (w e. NN -> ((F:NN-->A /\ G:NN-->B) -> ((F` w) e. A /\ (G` w) e. B)))
6		osumlem4.1	. . . . . . . . . . . . . . . . . . . . 21 |- A e. CH
7		osumlem4.2	. . . . . . . . . . . . . . . . . . . . 21 |- B e. CH
8		osumlem4.3	. . . . . . . . . . . . . . . . . . . . 21 |- B (_ (_|_` A)
9		pm4.2 170	. . . . . . . . . . . . . . . . . . . . 21 |- (((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +h (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) <-> ((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +h (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))))
10	6, 7, 8, 9	osumlem3 9580	. . . . . . . . . . . . . . . . . . . 20 |- (((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +h (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) -> (normh` ((G` w) -h y)) <_ (normh` ((H` w) -h z)))
11	10	adantr 389	. . . . . . . . . . . . . . . . . . 19 |- ((((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +h (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) /\ u e. RR) -> (normh` ((G` w) -h y)) <_ (normh` ((H` w) -h z)))
12	6, 7, 8, 9	osumlem1 9578	. . . . . . . . . . . . . . . . . . . . 21 |- (((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +h (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) -> ((((F` w) e. H~ /\ (G` w) e. H~) /\ (H` w) e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)))
13		lelttrt 5523	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((normh` ((G` w) -h y)) e. RR /\ (normh` ((H` w) -h z)) e. RR /\ u e. RR) -> (((normh` ((G` w) -h y)) <_ (normh` ((H` w) -h z)) /\ (normh` ((H` w) -h z)) < u) -> (normh` ((G` w) -h y)) < u))
14	13	3exp 832	. . . . . . . . . . . . . . . . . . . . . 22 |- ((normh` ((G` w) -h y)) e. RR -> ((normh` ((H` w) -h z)) e. RR -> (u e. RR -> (((normh` ((G` w) -h y)) <_ (normh` ((H` w) -h z)) /\ (normh` ((H` w) -h z)) < u) -> (normh` ((G` w) -h y)) < u))))
15		hvsubclt 8887	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((G` w) e. H~ /\ y e. H~) -> ((G` w) -h y) e. H~)
16		normclt 8991	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((G` w) -h y) e. H~ -> (normh` ((G` w) -h y)) e. RR)
17	15, 16	syl 10	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((G` w) e. H~ /\ y e. H~) -> (normh` ((G` w) -h y)) e. RR)
18	17	ad2ant2l 408	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((F` w) e. H~ /\ (G` w) e. H~) /\ (x e. H~ /\ y e. H~)) -> (normh` ((G` w) -h y)) e. RR)
19	18	ad2ant2r 409	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((F` w) e. H~ /\ (G` w) e. H~) /\ (H` w) e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (normh` ((G` w) -h y)) e. RR)
20		hvsubclt 8887	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((H` w) e. H~ /\ z e. H~) -> ((H` w) -h z) e. H~)
21		normclt 8991	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((H` w) -h z) e. H~ -> (normh` ((H` w) -h z)) e. RR)
22	20, 21	syl 10	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((H` w) e. H~ /\ z e. H~) -> (normh` ((H` w) -h z)) e. RR)
23	22	ad2ant2l 408	. . . . . . . . . . . . . . . . . . . . . 22 |- (((((F` w) e. H~ /\ (G` w) e. H~) /\ (H` w) e. H~) /\ ((x e. H~ /\ y e. H~) /\ z e. H~)) -> (normh` ((H` w) -h z)) e. RR)
24	14, 19, 23	sylc 68	. . . . . . . . . . . . . . . . . . . . 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 -> (((normh` ((G` w) -h y)) <_ (normh` ((H` w) -h z)) /\ (normh` ((H` w) -h z)) < u) -> (normh` ((G` w) -h y)) < u)))
25	12, 24	syl 10	. . . . . . . . . . . . . . . . . . . 20 |- (((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +h (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) -> (u e. RR -> (((normh` ((G` w) -h y)) <_ (normh` ((H` w) -h z)) /\ (normh` ((H` w) -h z)) < u) -> (normh` ((G` w) -h y)) < u)))
26	25	imp 350	. . . . . . . . . . . . . . . . . . 19 |- ((((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +h (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) /\ u e. RR) -> (((normh` ((G` w) -h y)) <_ (normh` ((H` w) -h z)) /\ (normh` ((H` w) -h z)) < u) -> (normh` ((G` w) -h y)) < u))
27	11, 26	mpand 701	. . . . . . . . . . . . . . . . . 18 |- ((((((F` w) e. A /\ (G` w) e. B) /\ (H` w) = ((F` w) +h (G` w))) /\ ((x e. A /\ y e. (_|_` A)) /\ z = (x +h y))) /\ u e. RR) -> ((normh` ((H` w) -h z)) < u -> (normh` ((G` w) -h y)) < u))
28	27	exp41 382	. . . . . . . . . . . . . . . . 17 |- (((F` w) e. A /\ (G` w) e. B) -> ((H` w) = ((F` w) +h (G` w)) -> (((x e. A /\ y e. (_|_` A)) /\ z = (x +h y)) -> (u e. RR -> ((normh` ((H` w) -h z)) < u -> (normh` ((G` w) -h y)) < u)))))
29	28	com24 37	. . . . . . . . . . . . . . . 16 |- (((F` w) e. A /\ (G` w) e. B) -> (u e. RR -> (((x e. A /\ y e. (_|_` A)) /\ z = (x +h y)) -> ((H` w) = ((F` w) +h (G` w)) -> ((normh` ((H` w) -h z)) < u -> (normh` ((G` w) -h y)) < u)))))
30	5, 29	syl6 22	. . . . . . . . . . . . . . 15 |- (w e. NN -> ((F:NN-->A /\ G:NN-->B) -> (u e. RR -> (((x e. A /\ y e. (_|_` A)) /\ z = (x +h y)) -> ((H` w) = ((F` w) +h (G` w)) -> ((normh` ((H` w) -h z)) < u -> (normh` ((G` w) -h y)) < u))))))
31	30	com4l 39	. . . . . . . . . . . . . 14 |- ((F:NN-->A /\ G:NN-->B) -> (u e. RR