cnlnadjlem2

Description: Lemma for cnlnadji . G is a continuous linear functional. (Contributed by NM, 16-Feb-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cnlnadjlem.1	$⊢ T \in LinOp$
	cnlnadjlem.2	$⊢ T \in ContOp$
	cnlnadjlem.3	$⊢ G = (g \in ℋ ⟼ T (g) \cdot_{ih} y)$
Assertion	cnlnadjlem2	$⊢ y \in ℋ \to (G \in LinFn \land G \in ContFn)$

Proof

Step	Hyp	Ref	Expression
1		cnlnadjlem.1	$⊢ T \in LinOp$
2		cnlnadjlem.2	$⊢ T \in ContOp$
3		cnlnadjlem.3	$⊢ G = (g \in ℋ ⟼ T (g) \cdot_{ih} y)$
4	1	lnopfi	$⊢ T : ℋ ⟶ ℋ$
5	4	ffvelrni	$⊢ g \in ℋ \to T (g) \in ℋ$
6		hicl	$⊢ (T (g) \in ℋ \land y \in ℋ) \to T (g) \cdot_{ih} y \in ℂ$
7	5 6	sylan	$⊢ (g \in ℋ \land y \in ℋ) \to T (g) \cdot_{ih} y \in ℂ$
8	7	ancoms	$⊢ (y \in ℋ \land g \in ℋ) \to T (g) \cdot_{ih} y \in ℂ$
9	8 3	fmptd	$⊢ y \in ℋ \to G : ℋ ⟶ ℂ$
10		hvmulcl	$⊢ (x \in ℂ \land w \in ℋ) \to x \cdot_{ℎ} w \in ℋ$
11	1	lnopaddi	$⊢ (x \cdot_{ℎ} w \in ℋ \land z \in ℋ) \to T ((x \cdot_{ℎ} w) +_{ℎ} z) = T (x \cdot_{ℎ} w) +_{ℎ} T (z)$
12	11	3adant3	$⊢ (x \cdot_{ℎ} w \in ℋ \land z \in ℋ \land y \in ℋ) \to T ((x \cdot_{ℎ} w) +_{ℎ} z) = T (x \cdot_{ℎ} w) +_{ℎ} T (z)$
13	12	oveq1d	$⊢ (x \cdot_{ℎ} w \in ℋ \land z \in ℋ \land y \in ℋ) \to T ((x \cdot_{ℎ} w) +_{ℎ} z) \cdot_{ih} y = (T (x \cdot_{ℎ} w) +_{ℎ} T (z)) \cdot_{ih} y$
14	4	ffvelrni	$⊢ x \cdot_{ℎ} w \in ℋ \to T (x \cdot_{ℎ} w) \in ℋ$
15	4	ffvelrni	$⊢ z \in ℋ \to T (z) \in ℋ$
16		id	$⊢ y \in ℋ \to y \in ℋ$
17		ax-his2	$⊢ (T (x \cdot_{ℎ} w) \in ℋ \land T (z) \in ℋ \land y \in ℋ) \to (T (x \cdot_{ℎ} w) +_{ℎ} T (z)) \cdot_{ih} y = (T (x \cdot_{ℎ} w) \cdot_{ih} y) + (T (z) \cdot_{ih} y)$
18	14 15 16 17	syl3an	$⊢ (x \cdot_{ℎ} w \in ℋ \land z \in ℋ \land y \in ℋ) \to (T (x \cdot_{ℎ} w) +_{ℎ} T (z)) \cdot_{ih} y = (T (x \cdot_{ℎ} w) \cdot_{ih} y) + (T (z) \cdot_{ih} y)$
19	13 18	eqtrd	$⊢ (x \cdot_{ℎ} w \in ℋ \land z \in ℋ \land y \in ℋ) \to T ((x \cdot_{ℎ} w) +_{ℎ} z) \cdot_{ih} y = (T (x \cdot_{ℎ} w) \cdot_{ih} y) + (T (z) \cdot_{ih} y)$
20	19	3comr	$⊢ (y \in ℋ \land x \cdot_{ℎ} w \in ℋ \land z \in ℋ) \to T ((x \cdot_{ℎ} w) +_{ℎ} z) \cdot_{ih} y = (T (x \cdot_{ℎ} w) \cdot_{ih} y) + (T (z) \cdot_{ih} y)$
21	20	3expa	$⊢ ((y \in ℋ \land x \cdot_{ℎ} w \in ℋ) \land z \in ℋ) \to T ((x \cdot_{ℎ} w) +_{ℎ} z) \cdot_{ih} y = (T (x \cdot_{ℎ} w) \cdot_{ih} y) + (T (z) \cdot_{ih} y)$
22	10 21	sylanl2	$⊢ ((y \in ℋ \land (x \in ℂ \land w \in ℋ)) \land z \in ℋ) \to T ((x \cdot_{ℎ} w) +_{ℎ} z) \cdot_{ih} y = (T (x \cdot_{ℎ} w) \cdot_{ih} y) + (T (z) \cdot_{ih} y)$
23		hvaddcl	$⊢ (x \cdot_{ℎ} w \in ℋ \land z \in ℋ) \to (x \cdot_{ℎ} w) +_{ℎ} z \in ℋ$
24	10 23	sylan	$⊢ ((x \in ℂ \land w \in ℋ) \land z \in ℋ) \to (x \cdot_{ℎ} w) +_{ℎ} z \in ℋ$
25	1 2 3	cnlnadjlem1	$⊢ (x \cdot_{ℎ} w) +_{ℎ} z \in ℋ \to G ((x \cdot_{ℎ} w) +_{ℎ} z) = T ((x \cdot_{ℎ} w) +_{ℎ} z) \cdot_{ih} y$
26	24 25	syl	$⊢ ((x \in ℂ \land w \in ℋ) \land z \in ℋ) \to G ((x \cdot_{ℎ} w) +_{ℎ} z) = T ((x \cdot_{ℎ} w) +_{ℎ} z) \cdot_{ih} y$
27	26	adantll	$⊢ ((y \in ℋ \land (x \in ℂ \land w \in ℋ)) \land z \in ℋ) \to G ((x \cdot_{ℎ} w) +_{ℎ} z) = T ((x \cdot_{ℎ} w) +_{ℎ} z) \cdot_{ih} y$
28	4	ffvelrni	$⊢ w \in ℋ \to T (w) \in ℋ$
29		ax-his3	$⊢ (x \in ℂ \land T (w) \in ℋ \land y \in ℋ) \to (x \cdot_{ℎ} T (w)) \cdot_{ih} y = x (T (w) \cdot_{ih} y)$
30	28 29	syl3an2	$⊢ (x \in ℂ \land w \in ℋ \land y \in ℋ) \to (x \cdot_{ℎ} T (w)) \cdot_{ih} y = x (T (w) \cdot_{ih} y)$
31	30	3comr	$⊢ (y \in ℋ \land x \in ℂ \land w \in ℋ) \to (x \cdot_{ℎ} T (w)) \cdot_{ih} y = x (T (w) \cdot_{ih} y)$
32	31	3expb	$⊢ (y \in ℋ \land (x \in ℂ \land w \in ℋ)) \to (x \cdot_{ℎ} T (w)) \cdot_{ih} y = x (T (w) \cdot_{ih} y)$
33	1	lnopmuli	$⊢ (x \in ℂ \land w \in ℋ) \to T (x \cdot_{ℎ} w) = x \cdot_{ℎ} T (w)$
34	33	oveq1d	$⊢ (x \in ℂ \land w \in ℋ) \to T (x \cdot_{ℎ} w) \cdot_{ih} y = (x \cdot_{ℎ} T (w)) \cdot_{ih} y$
35	34	adantl	$⊢ (y \in ℋ \land (x \in ℂ \land w \in ℋ)) \to T (x \cdot_{ℎ} w) \cdot_{ih} y = (x \cdot_{ℎ} T (w)) \cdot_{ih} y$
36	1 2 3	cnlnadjlem1	$⊢ w \in ℋ \to G (w) = T (w) \cdot_{ih} y$
37	36	oveq2d	$⊢ w \in ℋ \to x G (w) = x (T (w) \cdot_{ih} y)$
38	37	ad2antll	$⊢ (y \in ℋ \land (x \in ℂ \land w \in ℋ)) \to x G (w) = x (T (w) \cdot_{ih} y)$
39	32 35 38	3eqtr4rd	$⊢ (y \in ℋ \land (x \in ℂ \land w \in ℋ)) \to x G (w) = T (x \cdot_{ℎ} w) \cdot_{ih} y$
40	1 2 3	cnlnadjlem1	$⊢ z \in ℋ \to G (z) = T (z) \cdot_{ih} y$
41	39 40	oveqan12d	$⊢ ((y \in ℋ \land (x \in ℂ \land w \in ℋ)) \land z \in ℋ) \to x G (w) + G (z) = (T (x \cdot_{ℎ} w) \cdot_{ih} y) + (T (z) \cdot_{ih} y)$
42	22 27 41	3eqtr4d	$⊢ ((y \in ℋ \land (x \in ℂ \land w \in ℋ)) \land z \in ℋ) \to G ((x \cdot_{ℎ} w) +_{ℎ} z) = x G (w) + G (z)$
43	42	ralrimiva	$⊢ (y \in ℋ \land (x \in ℂ \land w \in ℋ)) \to \forall z \in ℋ G ((x \cdot_{ℎ} w) +_{ℎ} z) = x G (w) + G (z)$
44	43	ralrimivva	$⊢ y \in ℋ \to \forall x \in ℂ \forall w \in ℋ \forall z \in ℋ G ((x \cdot_{ℎ} w) +_{ℎ} z) = x G (w) + G (z)$
45		ellnfn	$⊢ G \in LinFn \leftrightarrow (G : ℋ ⟶ ℂ \land \forall x \in ℂ \forall w \in ℋ \forall z \in ℋ G ((x \cdot_{ℎ} w) +_{ℎ} z) = x G (w) + G (z))$
46	9 44 45	sylanbrc	$⊢ y \in ℋ \to G \in LinFn$
47	1 2	nmcopexi	$⊢ {norm}_{op} (T) \in ℝ$
48		normcl	$⊢ y \in ℋ \to {norm}_{ℎ} (y) \in ℝ$
49		remulcl	$⊢ ({norm}_{op} (T) \in ℝ \land {norm}_{ℎ} (y) \in ℝ) \to {norm}_{op} (T) {norm}_{ℎ} (y) \in ℝ$
50	47 48 49	sylancr	$⊢ y \in ℋ \to {norm}_{op} (T) {norm}_{ℎ} (y) \in ℝ$
51	40	adantr	$⊢ (z \in ℋ \land y \in ℋ) \to G (z) = T (z) \cdot_{ih} y$
52		hicl	$⊢ (T (z) \in ℋ \land y \in ℋ) \to T (z) \cdot_{ih} y \in ℂ$
53	15 52	sylan	$⊢ (z \in ℋ \land y \in ℋ) \to T (z) \cdot_{ih} y \in ℂ$
54	51 53	eqeltrd	$⊢ (z \in ℋ \land y \in ℋ) \to G (z) \in ℂ$
55	54	abscld	$⊢ (z \in ℋ \land y \in ℋ) \to \|G (z)\| \in ℝ$
56		normcl	$⊢ T (z) \in ℋ \to {norm}_{ℎ} (T (z)) \in ℝ$
57	15 56	syl	$⊢ z \in ℋ \to {norm}_{ℎ} (T (z)) \in ℝ$
58		remulcl	$⊢ ({norm}_{ℎ} (T (z)) \in ℝ \land {norm}_{ℎ} (y) \in ℝ) \to {norm}_{ℎ} (T (z)) {norm}_{ℎ} (y) \in ℝ$
59	57 48 58	syl2an	$⊢ (z \in ℋ \land y \in ℋ) \to {norm}_{ℎ} (T (z)) {norm}_{ℎ} (y) \in ℝ$
60		normcl	$⊢ z \in ℋ \to {norm}_{ℎ} (z) \in ℝ$
61		remulcl	$⊢ ({norm}_{op} (T) \in ℝ \land {norm}_{ℎ} (z) \in ℝ) \to {norm}_{op} (T) {norm}_{ℎ} (z) \in ℝ$
62	47 60 61	sylancr	$⊢ z \in ℋ \to {norm}_{op} (T) {norm}_{ℎ} (z) \in ℝ$
63		remulcl	$⊢ ({norm}_{op} (T) {norm}_{ℎ} (z) \in ℝ \land {norm}_{ℎ} (y) \in ℝ) \to {norm}_{op} (T) {norm}_{ℎ} (z) {norm}_{ℎ} (y) \in ℝ$
64	62 48 63	syl2an	$⊢ (z \in ℋ \land y \in ℋ) \to {norm}_{op} (T) {norm}_{ℎ} (z) {norm}_{ℎ} (y) \in ℝ$
65	51	fveq2d	$⊢ (z \in ℋ \land y \in ℋ) \to \|G (z)\| = \|T (z) \cdot_{ih} y\|$
66		bcs	$⊢ (T (z) \in ℋ \land y \in ℋ) \to \|T (z) \cdot_{ih} y\| \leq {norm}_{ℎ} (T (z)) {norm}_{ℎ} (y)$
67	15 66	sylan	$⊢ (z \in ℋ \land y \in ℋ) \to \|T (z) \cdot_{ih} y\| \leq {norm}_{ℎ} (T (z)) {norm}_{ℎ} (y)$
68	65 67	eqbrtrd	$⊢ (z \in ℋ \land y \in ℋ) \to \|G (z)\| \leq {norm}_{ℎ} (T (z)) {norm}_{ℎ} (y)$
69	57	adantr	$⊢ (z \in ℋ \land y \in ℋ) \to {norm}_{ℎ} (T (z)) \in ℝ$
70	62	adantr	$⊢ (z \in ℋ \land y \in ℋ) \to {norm}_{op} (T) {norm}_{ℎ} (z) \in ℝ$
71		normge0	$⊢ y \in ℋ \to 0 \leq {norm}_{ℎ} (y)$
72	48 71	jca	$⊢ y \in ℋ \to ({norm}_{ℎ} (y) \in ℝ \land 0 \leq {norm}_{ℎ} (y))$
73	72	adantl	$⊢ (z \in ℋ \land y \in ℋ) \to ({norm}_{ℎ} (y) \in ℝ \land 0 \leq {norm}_{ℎ} (y))$
74	1 2	nmcoplbi	$⊢ z \in ℋ \to {norm}_{ℎ} (T (z)) \leq {norm}_{op} (T) {norm}_{ℎ} (z)$
75	74	adantr	$⊢ (z \in ℋ \land y \in ℋ) \to {norm}_{ℎ} (T (z)) \leq {norm}_{op} (T) {norm}_{ℎ} (z)$
76		lemul1a	$⊢ (({norm}_{ℎ} (T (z)) \in ℝ \land {norm}_{op} (T) {norm}_{ℎ} (z) \in ℝ \land ({norm}_{ℎ} (y) \in ℝ \land 0 \leq {norm}_{ℎ} (y))) \land {norm}_{ℎ} (T (z)) \leq {norm}_{op} (T) {norm}_{ℎ} (z)) \to {norm}_{ℎ} (T (z)) {norm}_{ℎ} (y) \leq {norm}_{op} (T) {norm}_{ℎ} (z) {norm}_{ℎ} (y)$
77	69 70 73 75 76	syl31anc	$⊢ (z \in ℋ \land y \in ℋ) \to {norm}_{ℎ} (T (z)) {norm}_{ℎ} (y) \leq {norm}_{op} (T) {norm}_{ℎ} (z) {norm}_{ℎ} (y)$
78	55 59 64 68 77	letrd	$⊢ (z \in ℋ \land y \in ℋ) \to \|G (z)\| \leq {norm}_{op} (T) {norm}_{ℎ} (z) {norm}_{ℎ} (y)$
79	60	recnd	$⊢ z \in ℋ \to {norm}_{ℎ} (z) \in ℂ$
80	48	recnd	$⊢ y \in ℋ \to {norm}_{ℎ} (y) \in ℂ$
81	47	recni	$⊢ {norm}_{op} (T) \in ℂ$
82		mul32	$⊢ ({norm}_{op} (T) \in ℂ \land {norm}_{ℎ} (z) \in ℂ \land {norm}_{ℎ} (y) \in ℂ) \to {norm}_{op} (T) {norm}_{ℎ} (z) {norm}_{ℎ} (y) = {norm}_{op} (T) {norm}_{ℎ} (y) {norm}_{ℎ} (z)$
83	81 82	mp3an1	$⊢ ({norm}_{ℎ} (z) \in ℂ \land {norm}_{ℎ} (y) \in ℂ) \to {norm}_{op} (T) {norm}_{ℎ} (z) {norm}_{ℎ} (y) = {norm}_{op} (T) {norm}_{ℎ} (y) {norm}_{ℎ} (z)$
84	79 80 83	syl2an	$⊢ (z \in ℋ \land y \in ℋ) \to {norm}_{op} (T) {norm}_{ℎ} (z) {norm}_{ℎ} (y) = {norm}_{op} (T) {norm}_{ℎ} (y) {norm}_{ℎ} (z)$
85	78 84	breqtrd	$⊢ (z \in ℋ \land y \in ℋ) \to \|G (z)\| \leq {norm}_{op} (T) {norm}_{ℎ} (y) {norm}_{ℎ} (z)$
86	85	ancoms	$⊢ (y \in ℋ \land z \in ℋ) \to \|G (z)\| \leq {norm}_{op} (T) {norm}_{ℎ} (y) {norm}_{ℎ} (z)$
87	86	ralrimiva	$⊢ y \in ℋ \to \forall z \in ℋ \|G (z)\| \leq {norm}_{op} (T) {norm}_{ℎ} (y) {norm}_{ℎ} (z)$
88		oveq1	$⊢ x = {norm}_{op} (T) {norm}_{ℎ} (y) \to x {norm}_{ℎ} (z) = {norm}_{op} (T) {norm}_{ℎ} (y) {norm}_{ℎ} (z)$
89	88	breq2d	$⊢ x = {norm}_{op} (T) {norm}_{ℎ} (y) \to (\|G (z)\| \leq x {norm}_{ℎ} (z) \leftrightarrow \|G (z)\| \leq {norm}_{op} (T) {norm}_{ℎ} (y) {norm}_{ℎ} (z))$
90	89	ralbidv	$⊢ x = {norm}_{op} (T) {norm}_{ℎ} (y) \to (\forall z \in ℋ \|G (z)\| \leq x {norm}_{ℎ} (z) \leftrightarrow \forall z \in ℋ \|G (z)\| \leq {norm}_{op} (T) {norm}_{ℎ} (y) {norm}_{ℎ} (z))$
91	90	rspcev	$⊢ ({norm}_{op} (T) {norm}_{ℎ} (y) \in ℝ \land \forall z \in ℋ \|G (z)\| \leq {norm}_{op} (T) {norm}_{ℎ} (y) {norm}_{ℎ} (z)) \to \exists x \in ℝ \forall z \in ℋ \|G (z)\| \leq x {norm}_{ℎ} (z)$
92	50 87 91	syl2anc	$⊢ y \in ℋ \to \exists x \in ℝ \forall z \in ℋ \|G (z)\| \leq x {norm}_{ℎ} (z)$
93		lnfncon	$⊢ G \in LinFn \to (G \in ContFn \leftrightarrow \exists x \in ℝ \forall z \in ℋ \|G (z)\| \leq x {norm}_{ℎ} (z))$
94	46 93	syl	$⊢ y \in ℋ \to (G \in ContFn \leftrightarrow \exists x \in ℝ \forall z \in ℋ \|G (z)\| \leq x {norm}_{ℎ} (z))$
95	92 94	mpbird	$⊢ y \in ℋ \to G \in ContFn$
96	46 95	jca	$⊢ y \in ℋ \to (G \in LinFn \land G \in ContFn)$

Metamath Proof Explorer

Theorem cnlnadjlem2

Proof