pjthlem2

Description: Lemma for pjth . (Contributed by NM, 10-Oct-1999) (Revised by Mario Carneiro, 15-May-2014)

	Ref	Expression
Hypotheses	pjthlem.v	$⊢ V = {Base}_{W}$
	pjthlem.n	$⊢ N = norm (W)$
	pjthlem.p	$⊢ \underset{˙}{+} = +_{W}$
	pjthlem.m	$⊢ \underset{˙}{-} = -_{W}$
	pjthlem.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
	pjthlem.l	$⊢ L = LSubSp (W)$
	pjthlem.1	$⊢ φ \to W \in ℂHil$
	pjthlem.2	$⊢ φ \to U \in L$
	pjthlem.4	$⊢ φ \to A \in V$
	pjthlem.j	$⊢ J = TopOpen (W)$
	pjthlem.s	$⊢ \underset{˙}{\oplus} = LSSum (W)$
	pjthlem.o	$⊢ O = ocv (W)$
	pjthlem.3	$⊢ φ \to U \in Clsd (J)$
Assertion	pjthlem2	$⊢ φ \to A \in (U \underset{˙}{\oplus} O (U))$

Proof

Step	Hyp	Ref	Expression
1		pjthlem.v	$⊢ V = {Base}_{W}$
2		pjthlem.n	$⊢ N = norm (W)$
3		pjthlem.p	$⊢ \underset{˙}{+} = +_{W}$
4		pjthlem.m	$⊢ \underset{˙}{-} = -_{W}$
5		pjthlem.h	$⊢ \underset{˙}{,} = \cdot_{𝑖} (W)$
6		pjthlem.l	$⊢ L = LSubSp (W)$
7		pjthlem.1	$⊢ φ \to W \in ℂHil$
8		pjthlem.2	$⊢ φ \to U \in L$
9		pjthlem.4	$⊢ φ \to A \in V$
10		pjthlem.j	$⊢ J = TopOpen (W)$
11		pjthlem.s	$⊢ \underset{˙}{\oplus} = LSSum (W)$
12		pjthlem.o	$⊢ O = ocv (W)$
13		pjthlem.3	$⊢ φ \to U \in Clsd (J)$
14		hlcph	$⊢ W \in ℂHil \to W \in CPreHil$
15	7 14	syl	$⊢ φ \to W \in CPreHil$
16	8 6	eleqtrdi	$⊢ φ \to U \in LSubSp (W)$
17		hlcms	$⊢ W \in ℂHil \to W \in CMetSp$
18	7 17	syl	$⊢ φ \to W \in CMetSp$
19	1 6	lssss	$⊢ U \in L \to U \subseteq V$
20	8 19	syl	$⊢ φ \to U \subseteq V$
21		eqid	$⊢ W ↾_{𝑠} U = W ↾_{𝑠} U$
22	21 1 10	cmsss	$⊢ (W \in CMetSp \land U \subseteq V) \to (W ↾_{𝑠} U \in CMetSp \leftrightarrow U \in Clsd (J))$
23	18 20 22	syl2anc	$⊢ φ \to (W ↾_{𝑠} U \in CMetSp \leftrightarrow U \in Clsd (J))$
24	13 23	mpbird	$⊢ φ \to W ↾_{𝑠} U \in CMetSp$
25	1 4 2 15 16 24 9	minvec	$⊢ φ \to \exists! x \in U \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y)$
26		reurex	$⊢ \exists! x \in U \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y) \to \exists x \in U \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y)$
27	25 26	syl	$⊢ φ \to \exists x \in U \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y)$
28	15	adantr	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to W \in CPreHil$
29		cphlmod	$⊢ W \in CPreHil \to W \in LMod$
30	28 29	syl	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to W \in LMod$
31		lmodabl	$⊢ W \in LMod \to W \in Abel$
32	30 31	syl	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to W \in Abel$
33	8	adantr	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to U \in L$
34	33 19	syl	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to U \subseteq V$
35		simprl	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to x \in U$
36	34 35	sseldd	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to x \in V$
37	9	adantr	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to A \in V$
38	1 3 4	ablpncan3	$⊢ (W \in Abel \land (x \in V \land A \in V)) \to x \underset{˙}{+} (A \underset{˙}{-} x) = A$
39	32 36 37 38	syl12anc	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to x \underset{˙}{+} (A \underset{˙}{-} x) = A$
40	6	lsssssubg	$⊢ W \in LMod \to L \subseteq SubGrp (W)$
41	30 40	syl	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to L \subseteq SubGrp (W)$
42	41 33	sseldd	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to U \in SubGrp (W)$
43		cphphl	$⊢ W \in CPreHil \to W \in PreHil$
44	28 43	syl	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to W \in PreHil$
45	1 12 6	ocvlss	$⊢ (W \in PreHil \land U \subseteq V) \to O (U) \in L$
46	44 34 45	syl2anc	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to O (U) \in L$
47	41 46	sseldd	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to O (U) \in SubGrp (W)$
48	1 4	lmodvsubcl	$⊢ (W \in LMod \land A \in V \land x \in V) \to A \underset{˙}{-} x \in V$
49	30 37 36 48	syl3anc	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to A \underset{˙}{-} x \in V$
50	7	ad2antrr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land z \in U) \to W \in ℂHil$
51	33	adantr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land z \in U) \to U \in L$
52	49	adantr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land z \in U) \to A \underset{˙}{-} x \in V$
53		simpr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land z \in U) \to z \in U$
54		oveq2	$⊢ y = w \underset{˙}{+} x \to A \underset{˙}{-} y = A \underset{˙}{-} (w \underset{˙}{+} x)$
55	54	fveq2d	$⊢ y = w \underset{˙}{+} x \to N (A \underset{˙}{-} y) = N (A \underset{˙}{-} (w \underset{˙}{+} x))$
56	55	breq2d	$⊢ y = w \underset{˙}{+} x \to (N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y) \leftrightarrow N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} (w \underset{˙}{+} x)))$
57		simplrr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y)$
58	30	adantr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to W \in LMod$
59	33	adantr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to U \in L$
60		simpr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to w \in U$
61	35	adantr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to x \in U$
62	3 6	lssvacl	$⊢ ((W \in LMod \land U \in L) \land (w \in U \land x \in U)) \to w \underset{˙}{+} x \in U$
63	58 59 60 61 62	syl22anc	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to w \underset{˙}{+} x \in U$
64	56 57 63	rspcdva	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} (w \underset{˙}{+} x))$
65		lmodgrp	$⊢ W \in LMod \to W \in Grp$
66	30 65	syl	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to W \in Grp$
67	66	adantr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to W \in Grp$
68	37	adantr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to A \in V$
69	36	adantr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to x \in V$
70	34	sselda	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to w \in V$
71	1 3 4	grpsubsub4	$⊢ (W \in Grp \land (A \in V \land x \in V \land w \in V)) \to (A \underset{˙}{-} x) \underset{˙}{-} w = A \underset{˙}{-} (w \underset{˙}{+} x)$
72	67 68 69 70 71	syl13anc	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to (A \underset{˙}{-} x) \underset{˙}{-} w = A \underset{˙}{-} (w \underset{˙}{+} x)$
73	72	fveq2d	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to N ((A \underset{˙}{-} x) \underset{˙}{-} w) = N (A \underset{˙}{-} (w \underset{˙}{+} x))$
74	64 73	breqtrrd	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land w \in U) \to N (A \underset{˙}{-} x) \leq N ((A \underset{˙}{-} x) \underset{˙}{-} w)$
75	74	ralrimiva	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to \forall w \in U N (A \underset{˙}{-} x) \leq N ((A \underset{˙}{-} x) \underset{˙}{-} w)$
76	75	adantr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land z \in U) \to \forall w \in U N (A \underset{˙}{-} x) \leq N ((A \underset{˙}{-} x) \underset{˙}{-} w)$
77		eqid	$⊢ \frac{(A \underset{˙}{-} x) \underset{˙}{,} z}{(z \underset{˙}{,} z) + 1} = \frac{(A \underset{˙}{-} x) \underset{˙}{,} z}{(z \underset{˙}{,} z) + 1}$
78	1 2 3 4 5 6 50 51 52 53 76 77	pjthlem1	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land z \in U) \to (A \underset{˙}{-} x) \underset{˙}{,} z = 0$
79	28	adantr	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land z \in U) \to W \in CPreHil$
80		cphclm	$⊢ W \in CPreHil \to W \in CMod$
81	79 80	syl	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land z \in U) \to W \in CMod$
82		eqid	$⊢ Scalar (W) = Scalar (W)$
83	82	clm0	$⊢ W \in CMod \to 0 = 0_{Scalar (W)}$
84	81 83	syl	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land z \in U) \to 0 = 0_{Scalar (W)}$
85	78 84	eqtrd	$⊢ ((φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \land z \in U) \to (A \underset{˙}{-} x) \underset{˙}{,} z = 0_{Scalar (W)}$
86	85	ralrimiva	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to \forall z \in U (A \underset{˙}{-} x) \underset{˙}{,} z = 0_{Scalar (W)}$
87		eqid	$⊢ 0_{Scalar (W)} = 0_{Scalar (W)}$
88	1 5 82 87 12	elocv	$⊢ A \underset{˙}{-} x \in O (U) \leftrightarrow (U \subseteq V \land A \underset{˙}{-} x \in V \land \forall z \in U (A \underset{˙}{-} x) \underset{˙}{,} z = 0_{Scalar (W)})$
89	34 49 86 88	syl3anbrc	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to A \underset{˙}{-} x \in O (U)$
90	3 11	lsmelvali	$⊢ ((U \in SubGrp (W) \land O (U) \in SubGrp (W)) \land (x \in U \land A \underset{˙}{-} x \in O (U))) \to x \underset{˙}{+} (A \underset{˙}{-} x) \in (U \underset{˙}{\oplus} O (U))$
91	42 47 35 89 90	syl22anc	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to x \underset{˙}{+} (A \underset{˙}{-} x) \in (U \underset{˙}{\oplus} O (U))$
92	39 91	eqeltrrd	$⊢ (φ \land (x \in U \land \forall y \in U N (A \underset{˙}{-} x) \leq N (A \underset{˙}{-} y))) \to A \in (U \underset{˙}{\oplus} O (U))$
93	27 92	rexlimddv	$⊢ φ \to A \in (U \underset{˙}{\oplus} O (U))$

Metamath Proof Explorer

Theorem pjthlem2

Proof