Theorem nmoleub2lem

Description: Lemma for nmoleub2a and similar theorems. (Contributed by Mario Carneiro, 19-Oct-2015)

	Ref	Expression
Hypotheses	nmoleub2.n	|- N = ( S normOp T )
	nmoleub2.v	|- V = ( Base ` S )
	nmoleub2.l	|- L = ( norm ` S )
	nmoleub2.m	|- M = ( norm ` T )
	nmoleub2.g	|- G = ( Scalar ` S )
	nmoleub2.w	|- K = ( Base ` G )
	nmoleub2.s	|- ( ph -> S e. ( NrmMod i^i CMod ) )
	nmoleub2.t	|- ( ph -> T e. ( NrmMod i^i CMod ) )
	nmoleub2.f	|- ( ph -> F e. ( S LMHom T ) )
	nmoleub2.a	|- ( ph -> A e. RR* )
	nmoleub2.r	|- ( ph -> R e. RR+ )
	nmoleub2lem.5	|- ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> 0 <_ A )
	nmoleub2lem.6	|- ( ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) )
	nmoleub2lem.7	|- ( ( ph /\ x e. V ) -> ( ps -> ( L ` x ) <_ R ) )
Assertion	nmoleub2lem	|- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )

Proof

Step	Hyp	Ref	Expression
1		nmoleub2.n	|- N = ( S normOp T )
2		nmoleub2.v	|- V = ( Base ` S )
3		nmoleub2.l	|- L = ( norm ` S )
4		nmoleub2.m	|- M = ( norm ` T )
5		nmoleub2.g	|- G = ( Scalar ` S )
6		nmoleub2.w	|- K = ( Base ` G )
7		nmoleub2.s	|- ( ph -> S e. ( NrmMod i^i CMod ) )
8		nmoleub2.t	|- ( ph -> T e. ( NrmMod i^i CMod ) )
9		nmoleub2.f	|- ( ph -> F e. ( S LMHom T ) )
10		nmoleub2.a	|- ( ph -> A e. RR* )
11		nmoleub2.r	|- ( ph -> R e. RR+ )
12		nmoleub2lem.5	|- ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> 0 <_ A )
13		nmoleub2lem.6	|- ( ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) /\ ( y e. V /\ y =/= ( 0g ` S ) ) ) -> ( M ` ( F ` y ) ) <_ ( A x. ( L ` y ) ) )
14		nmoleub2lem.7	|- ( ( ph /\ x e. V ) -> ( ps -> ( L ` x ) <_ R ) )
15	14	adantlr	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ x e. V ) -> ( ps -> ( L ` x ) <_ R ) )
16	8	elin1d	|- ( ph -> T e. NrmMod )
17		nlmngp	|- ( T e. NrmMod -> T e. NrmGrp )
18	16 17	syl	|- ( ph -> T e. NrmGrp )
19	18	ad2antrr	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> T e. NrmGrp )
20		eqid	|- ( Base ` T ) = ( Base ` T )
21	2 20	lmhmf	|- ( F e. ( S LMHom T ) -> F : V --> ( Base ` T ) )
22	9 21	syl	|- ( ph -> F : V --> ( Base ` T ) )
23	22	ad2antrr	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> F : V --> ( Base ` T ) )
24		simprl	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> x e. V )
25	23 24	ffvelrnd	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( F ` x ) e. ( Base ` T ) )
26	20 4	nmcl	|- ( ( T e. NrmGrp /\ ( F ` x ) e. ( Base ` T ) ) -> ( M ` ( F ` x ) ) e. RR )
27	19 25 26	syl2anc	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( M ` ( F ` x ) ) e. RR )
28	11	ad2antrr	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> R e. RR+ )
29	27 28	rerpdivcld	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( M ` ( F ` x ) ) / R ) e. RR )
30	29	rexrd	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( M ` ( F ` x ) ) / R ) e. RR* )
31	7	elin1d	|- ( ph -> S e. NrmMod )
32		nlmngp	|- ( S e. NrmMod -> S e. NrmGrp )
33	31 32	syl	|- ( ph -> S e. NrmGrp )
34		lmghm	|- ( F e. ( S LMHom T ) -> F e. ( S GrpHom T ) )
35	9 34	syl	|- ( ph -> F e. ( S GrpHom T ) )
36	1	nmocl	|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> ( N ` F ) e. RR* )
37	33 18 35 36	syl3anc	|- ( ph -> ( N ` F ) e. RR* )
38	37	ad2antrr	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( N ` F ) e. RR* )
39	10	ad2antrr	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> A e. RR* )
40	28	rpred	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> R e. RR )
41		rexmul	|- ( ( ( ( M ` ( F ` x ) ) / R ) e. RR /\ R e. RR ) -> ( ( ( M ` ( F ` x ) ) / R ) *e R ) = ( ( ( M ` ( F ` x ) ) / R ) x. R ) )
42	29 40 41	syl2anc	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( ( M ` ( F ` x ) ) / R ) *e R ) = ( ( ( M ` ( F ` x ) ) / R ) x. R ) )
43	27	recnd	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( M ` ( F ` x ) ) e. CC )
44	40	recnd	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> R e. CC )
45	28	rpne0d	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> R =/= 0 )
46	43 44 45	divcan1d	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( ( M ` ( F ` x ) ) / R ) x. R ) = ( M ` ( F ` x ) ) )
47	42 46	eqtrd	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( ( M ` ( F ` x ) ) / R ) *e R ) = ( M ` ( F ` x ) ) )
48	27	rexrd	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( M ` ( F ` x ) ) e. RR* )
49	33	ad2antrr	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> S e. NrmGrp )
50	2 3	nmcl	|- ( ( S e. NrmGrp /\ x e. V ) -> ( L ` x ) e. RR )
51	49 24 50	syl2anc	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( L ` x ) e. RR )
52	51	rexrd	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( L ` x ) e. RR* )
53	38 52	xmulcld	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( N ` F ) *e ( L ` x ) ) e. RR* )
54	28	rpxrd	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> R e. RR* )
55	38 54	xmulcld	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( N ` F ) *e R ) e. RR* )
56	35	ad2antrr	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> F e. ( S GrpHom T ) )
57	1 2 3 4	nmoix	|- ( ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) /\ x e. V ) -> ( M ` ( F ` x ) ) <_ ( ( N ` F ) *e ( L ` x ) ) )
58	49 19 56 24 57	syl31anc	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( M ` ( F ` x ) ) <_ ( ( N ` F ) *e ( L ` x ) ) )
59	1	nmoge0	|- ( ( S e. NrmGrp /\ T e. NrmGrp /\ F e. ( S GrpHom T ) ) -> 0 <_ ( N ` F ) )
60	33 18 35 59	syl3anc	|- ( ph -> 0 <_ ( N ` F ) )
61	37 60	jca	|- ( ph -> ( ( N ` F ) e. RR* /\ 0 <_ ( N ` F ) ) )
62	61	ad2antrr	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( N ` F ) e. RR* /\ 0 <_ ( N ` F ) ) )
63		simprr	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( L ` x ) <_ R )
64		xlemul2a	|- ( ( ( ( L ` x ) e. RR* /\ R e. RR* /\ ( ( N ` F ) e. RR* /\ 0 <_ ( N ` F ) ) ) /\ ( L ` x ) <_ R ) -> ( ( N ` F ) *e ( L ` x ) ) <_ ( ( N ` F ) *e R ) )
65	52 54 62 63 64	syl31anc	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( N ` F ) *e ( L ` x ) ) <_ ( ( N ` F ) *e R ) )
66	48 53 55 58 65	xrletrd	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( M ` ( F ` x ) ) <_ ( ( N ` F ) *e R ) )
67	47 66	eqbrtrd	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( ( M ` ( F ` x ) ) / R ) *e R ) <_ ( ( N ` F ) *e R ) )
68		xlemul1	|- ( ( ( ( M ` ( F ` x ) ) / R ) e. RR* /\ ( N ` F ) e. RR* /\ R e. RR+ ) -> ( ( ( M ` ( F ` x ) ) / R ) <_ ( N ` F ) <-> ( ( ( M ` ( F ` x ) ) / R ) *e R ) <_ ( ( N ` F ) *e R ) ) )
69	30 38 28 68	syl3anc	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( ( M ` ( F ` x ) ) / R ) <_ ( N ` F ) <-> ( ( ( M ` ( F ` x ) ) / R ) *e R ) <_ ( ( N ` F ) *e R ) ) )
70	67 69	mpbird	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( M ` ( F ` x ) ) / R ) <_ ( N ` F ) )
71		simplr	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( N ` F ) <_ A )
72	30 38 39 70 71	xrletrd	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ ( x e. V /\ ( L ` x ) <_ R ) ) -> ( ( M ` ( F ` x ) ) / R ) <_ A )
73	72	expr	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ x e. V ) -> ( ( L ` x ) <_ R -> ( ( M ` ( F ` x ) ) / R ) <_ A ) )
74	15 73	syld	|- ( ( ( ph /\ ( N ` F ) <_ A ) /\ x e. V ) -> ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) )
75	74	ralrimiva	|- ( ( ph /\ ( N ` F ) <_ A ) -> A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) )
76		eqid	|- ( 0g ` S ) = ( 0g ` S )
77	33	ad2antrr	|- ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) -> S e. NrmGrp )
78	18	ad2antrr	|- ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) -> T e. NrmGrp )
79	35	ad2antrr	|- ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) -> F e. ( S GrpHom T ) )
80		simpr	|- ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) -> A e. RR )
81	12	adantr	|- ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) -> 0 <_ A )
82	1 2 3 4 76 77 78 79 80 81 13	nmolb2d	|- ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A e. RR ) -> ( N ` F ) <_ A )
83	37	ad2antrr	|- ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A = +oo ) -> ( N ` F ) e. RR* )
84		pnfge	|- ( ( N ` F ) e. RR* -> ( N ` F ) <_ +oo )
85	83 84	syl	|- ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A = +oo ) -> ( N ` F ) <_ +oo )
86		simpr	|- ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A = +oo ) -> A = +oo )
87	85 86	breqtrrd	|- ( ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) /\ A = +oo ) -> ( N ` F ) <_ A )
88	10	adantr	|- ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> A e. RR* )
89		ge0nemnf	|- ( ( A e. RR* /\ 0 <_ A ) -> A =/= -oo )
90	88 12 89	syl2anc	|- ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> A =/= -oo )
91	88 90	jca	|- ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( A e. RR* /\ A =/= -oo ) )
92		xrnemnf	|- ( ( A e. RR* /\ A =/= -oo ) <-> ( A e. RR \/ A = +oo ) )
93	91 92	sylib	|- ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( A e. RR \/ A = +oo ) )
94	82 87 93	mpjaodan	|- ( ( ph /\ A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) -> ( N ` F ) <_ A )
95	75 94	impbida	|- ( ph -> ( ( N ` F ) <_ A <-> A. x e. V ( ps -> ( ( M ` ( F ` x ) ) / R ) <_ A ) ) )