Theorem bopcnlem2 7982

Description: Lemma for bopcn 7985.

Hypotheses

Ref	Expression
bopcn.1	|- C = (abs o. - )
bopcn.2	|- D = {<.<.w, v>., u>. | ((w e. (CC X. CC) /\ v e. (CC X. CC)) /\ u = sup({((1st` w)C(1st` v)), ((2nd` w)C(2nd` v))}, RR, < ))}
bopcn.j	|- J = (Open` C)
bopcn.k	|- K = (Open` D)
bopcn.5	|- O:(CC X. CC)-->CC
bopcn.6	|- F = {<.k, r>. | (k e. NN /\ r = (1st` (h` k)))}
bopcn.7	|- G = {<.k, r>. | (k e. NN /\ r = (2nd` (h` k)))}
bopcn.9	|- (((1st` (h` k)) e. CC /\ (2nd` (h` k)) e. CC) -> ((1st` (h` k))O(2nd` (h` k))) e. CC)
bopcn.10	|- (((F ~~> (1st` q) /\ G ~~> (2nd` q)) /\ (1 e. ZZ /\ A.m e. (ZZ>` 1)((F` m) e. CC /\ (G` m) e. CC /\ (H` m) = ((F` m)O(G` m))))) -> H ~~> ((1st` q)O(2nd` q)))
bopcn.8	|- H = {<.k, r>. | (k e. NN /\ r = (O` (h` k)))}

Assertion

Ref	Expression
bopcnlem2	|- ((h:NN-->(CC X. CC) /\ h(~~>m` D)q) -> H ~~> ((1st` q)O(2nd` q)))

Distinct variable groups:   h,q,u,v,w,C   h,m,D,q   u,m,v,w,F   m,G,u,v,w   H,q   J,q   K,q   h,k,r,O,q   k,m,u,v,w,r

Proof of Theorem bopcnlem2

Step	Hyp	Ref	Expression
1		bopcn.1	. . 3 |- C = (abs o. - )
2		bopcn.2	. . 3 |- D = {<.<.w, v>., u>. | ((w e. (CC X. CC) /\ v e. (CC X. CC)) /\ u = sup({((1st` w)C(1st` v)), ((2nd` w)C(2nd` v))}, RR, < ))}
3		bopcn.j	. . 3 |- J = (Open` C)
4		bopcn.k	. . 3 |- K = (Open` D)
5		bopcn.5	. . 3 |- O:(CC X. CC)-->CC
6		bopcn.6	. . 3 |- F = {<.k, r>. | (k e. NN /\ r = (1st` (h` k)))}
7		bopcn.7	. . 3 |- G = {<.k, r>. | (k e. NN /\ r = (2nd` (h` k)))}
8		bopcn.9	. . 3 |- (((1st` (h` k)) e. CC /\ (2nd` (h` k)) e. CC) -> ((1st` (h` k))O(2nd` (h` k))) e. CC)
9		bopcn.10	. . 3 |- (((F ~~> (1st` q) /\ G ~~> (2nd` q)) /\ (1 e. ZZ /\ A.m e. (ZZ>` 1)((F` m) e. CC /\ (G` m) e. CC /\ (H` m) = ((F` m)O(G` m))))) -> H ~~> ((1st` q)O(2nd` q)))
10		bopcn.8	. . 3 |- H = {<.k, r>. | (k e. NN /\ r = (O` (h` k)))}
11	1, 2, 3, 4, 5, 6, 7, 8, 9, 10	bopcnlem1 7981	. 2 |- ((h:NN-->(CC X. CC) /\ h(~~>m` D)q) -> ((F:NN-->CC /\ F ~~> (1st` q)) /\ (G:NN-->CC /\ G ~~> (2nd` q))))
12		1z 6159	. . . 4 |- 1 e. ZZ
13	12, 9	mpanr1 709	. . 3 |- (((F ~~> (1st` q) /\ G ~~> (2nd` q)) /\ A.m e. (ZZ>` 1)((F` m) e. CC /\ (G` m) e. CC /\ (H` m) = ((F` m)O(G` m)))) -> H ~~> ((1st` q)O(2nd` q)))
14		pm3.27 323	. . . . 5 |- ((F:NN-->CC /\ F ~~> (1st` q)) -> F ~~> (1st` q))
15		pm3.27 323	. . . . 5 |- ((G:NN-->CC /\ G ~~> (2nd` q)) -> G ~~> (2nd` q))
16	14, 15	anim12i 333	. . . 4 |- (((F:NN-->CC /\ F ~~> (1st` q)) /\ (G:NN-->CC /\ G ~~> (2nd` q))) -> (F ~~> (1st` q) /\ G ~~> (2nd` q)))
17	16	adantl 388	. . 3 |- (((h:NN-->(CC X. CC) /\ h(~~>m` D)q) /\ ((F:NN-->CC /\ F ~~> (1st` q)) /\ (G:NN-->CC /\ G ~~> (2nd` q)))) -> (F ~~> (1st` q) /\ G ~~> (2nd` q)))
18		ffvelrn 3814	. . . . . . . . . 10 |- ((F:NN-->CC /\ m e. NN) -> (F` m) e. CC)
19	18	adantlr 393	. . . . . . . . 9 |- (((F:NN-->CC /\ G:NN-->CC) /\ m e. NN) -> (F` m) e. CC)
20	19	adantll 392	. . . . . . . 8 |- ((((h:NN-->(CC X. CC) /\ h(~~>m` D)q) /\ (F:NN-->CC /\ G:NN-->CC)) /\ m e. NN) -> (F` m) e. CC)
21		ffvelrn 3814	. . . . . . . . . 10 |- ((G:NN-->CC /\ m e. NN) -> (G` m) e. CC)
22	21	adantll 392	. . . . . . . . 9 |- (((F:NN-->CC /\ G:NN-->CC) /\ m e. NN) -> (G` m) e. CC)
23	22	adantll 392	. . . . . . . 8 |- ((((h:NN-->(CC X. CC) /\ h(~~>m` D)q) /\ (F:NN-->CC /\ G:NN-->CC)) /\ m e. NN) -> (G` m) e. CC)
24		ffvelrn 3814	. . . . . . . . . . . . . 14 |- ((h:NN-->(CC X. CC) /\ m e. NN) -> (h` m) e. (CC X. CC))
25		elxp6 4102	. . . . . . . . . . . . . . 15 |- ((h` m) e. (CC X. CC) <-> ((h` m) = <.(1st` (h` m)), (2nd` (h` m))>. /\ ((1st` (h` m)) e. CC /\ (2nd` (h` m)) e. CC)))
26	25	pm3.26bi 322	. . . . . . . . . . . . . 14 |- ((h` m) e. (CC X. CC) -> (h` m) = <.(1st` (h` m)), (2nd` (h` m))>.)
27	24, 26	syl 10	. . . . . . . . . . . . 13 |- ((h:NN-->(CC X. CC) /\ m e. NN) -> (h` m) = <.(1st` (h` m)), (2nd` (h` m))>.)
28	27	fveq2d 3728	. . . . . . . . . . . 12 |- ((h:NN-->(CC X. CC) /\ m e. NN) -> (O` (h` m)) = (O` <.(1st` (h` m)), (2nd` (h` m))>.))
29		df-opr 3965	. . . . . . . . . . . 12 |- ((1st` (h` m))O(2nd` (h` m))) = (O` <.(1st` (h` m)), (2nd` (h` m))>.)
30	28, 29	syl6eqr 1525	. . . . . . . . . . 11 |- ((h:NN-->(CC X. CC) /\ m e. NN) -> (O` (h` m)) = ((1st` (h` m))O(2nd` (h` m))))
31	30	adantlr 393	. . . . . . . . . 10 |- (((h:NN-->(CC X. CC) /\ h(~~>m` D)q) /\ m e. NN) -> (O` (h` m)) = ((1st` (h` m))O(2nd` (h` m))))
32	31	adantlr 393	. . . . . . . . 9 |- ((((h:NN-->(CC X. CC) /\ h(~~>m` D)q) /\ (F:NN-->CC /\ G:NN-->CC)) /\ m e. NN) -> (O` (h` m)) = ((1st` (h` m))O(2nd` (h` m))))
33		fveq2 3724	. . . . . . . . . . . 12 |- (k = m -> (h` k) = (h` m))
34	33	fveq2d 3728	. . . . . . . . . . 11 |- (k = m -> (O` (h` k)) = (O` (h` m)))
35		fvex 3732	. . . . . . . . . . 11 |- (O` (h` m)) e. V
36	34, 10, 35	fvopab4 3780	. . . . . . . . . 10 |- (m e. NN -> (H` m) = (O` (h` m)))
37	36	adantl 388	. . . . . . . . 9 |- ((((h:NN-->(CC X. CC) /\ h(~~>m` D)q) /\ (F:NN-->CC /\ G:NN-->CC)) /\ m e. NN) -> (H` m) = (O` (h` m)))
38	33	fveq2d 3728	. . . . . . . . . . . 12 |- (k = m -> (1st` (h` k)) = (1st` (h` m)))
39		fvex 3732	. . . . . . . . . . . 12 |- (1st` (h` m)) e. V
40	38, 6, 39	fvopab4 3780	. . . . . . . . . . 11 |- (m e. NN -> (F` m) = (1st` (h` m)))
41	33	fveq2d 3728	. . . . . . . . . . . 12 |- (k = m -> (2nd` (h` k)) = (2nd` (h` m)))
42		fvex 3732	. . . . . . . . . . . 12 |- (2nd` (h` m)) e. V
43	41, 7, 42	fvopab4 3780	. . . . . . . . . . 11 |- (m e. NN -> (G` m) = (2nd` (h` m)))
44	40, 43	opreq12d 3978	. . . . . . . . . 10 |- (m e. NN -> ((F` m)O(G` m)) = ((1st` (h` m))O(2nd` (h` m))))
45	44	adantl 388	. . . . . . . . 9 |- ((((h:NN-->(CC X. CC) /\ h(~~>m` D)q