hlhillcs

Description: The closed subspaces of the final constructed Hilbert space. TODO: hlhilbase is applied over and over to conclusion rather than applied once to antecedent - would compressed proof be shorter if applied once to antecedent? (Contributed by NM, 23-Jun-2015)

	Ref	Expression
Hypotheses	hlhillcs.h	$⊢ H = LHyp (K)$
	hlhillcs.i	$⊢ I = DIsoH (K) (W)$
	hlhillcs.u	$⊢ U = HLHil (K) (W)$
	hlhillcs.c	$⊢ C = ClSubSp (U)$
	hlhillcs.k	$⊢ φ \to (K \in HL \land W \in H)$
Assertion	hlhillcs	$⊢ φ \to C = ran I$

Proof

Step	Hyp	Ref	Expression
1		hlhillcs.h	$⊢ H = LHyp (K)$
2		hlhillcs.i	$⊢ I = DIsoH (K) (W)$
3		hlhillcs.u	$⊢ U = HLHil (K) (W)$
4		hlhillcs.c	$⊢ C = ClSubSp (U)$
5		hlhillcs.k	$⊢ φ \to (K \in HL \land W \in H)$
6	3	fvexi	$⊢ U \in V$
7		eqid	$⊢ ocv (U) = ocv (U)$
8	7 4	iscss	$⊢ U \in V \to (x \in C \leftrightarrow x = ocv (U) (ocv (U) (x)))$
9	6 8	mp1i	$⊢ φ \to (x \in C \leftrightarrow x = ocv (U) (ocv (U) (x)))$
10	9	biimpa	$⊢ (φ \land x \in C) \to x = ocv (U) (ocv (U) (x))$
11		eqid	$⊢ {Base}_{U} = {Base}_{U}$
12	11 4	cssss	$⊢ x \in C \to x \subseteq {Base}_{U}$
13		eqid	$⊢ DVecH (K) (W) = DVecH (K) (W)$
14		eqid	$⊢ {Base}_{DVecH (K) (W)} = {Base}_{DVecH (K) (W)}$
15		eqid	$⊢ ocH (K) (W) = ocH (K) (W)$
16	5	adantr	$⊢ (φ \land x \subseteq {Base}_{U}) \to (K \in HL \land W \in H)$
17	1 3 5 13 14	hlhilbase	$⊢ φ \to {Base}_{DVecH (K) (W)} = {Base}_{U}$
18	17	sseq2d	$⊢ φ \to (x \subseteq {Base}_{DVecH (K) (W)} \leftrightarrow x \subseteq {Base}_{U})$
19	18	biimpar	$⊢ (φ \land x \subseteq {Base}_{U}) \to x \subseteq {Base}_{DVecH (K) (W)}$
20	1 2 13 14 15 16 19	dochoccl	$⊢ (φ \land x \subseteq {Base}_{U}) \to (x \in ran I \leftrightarrow ocH (K) (W) (ocH (K) (W) (x)) = x)$
21		eqcom	$⊢ x = ocv (U) (ocv (U) (x)) \leftrightarrow ocv (U) (ocv (U) (x)) = x$
22	1 13 3 16 14 15 7 19	hlhilocv	$⊢ (φ \land x \subseteq {Base}_{U}) \to ocv (U) (x) = ocH (K) (W) (x)$
23	22	fveq2d	$⊢ (φ \land x \subseteq {Base}_{U}) \to ocv (U) (ocv (U) (x)) = ocv (U) (ocH (K) (W) (x))$
24	1 13 14 15	dochssv	$⊢ ((K \in HL \land W \in H) \land x \subseteq {Base}_{DVecH (K) (W)}) \to ocH (K) (W) (x) \subseteq {Base}_{DVecH (K) (W)}$
25	16 19 24	syl2anc	$⊢ (φ \land x \subseteq {Base}_{U}) \to ocH (K) (W) (x) \subseteq {Base}_{DVecH (K) (W)}$
26	1 13 3 16 14 15 7 25	hlhilocv	$⊢ (φ \land x \subseteq {Base}_{U}) \to ocv (U) (ocH (K) (W) (x)) = ocH (K) (W) (ocH (K) (W) (x))$
27	23 26	eqtrd	$⊢ (φ \land x \subseteq {Base}_{U}) \to ocv (U) (ocv (U) (x)) = ocH (K) (W) (ocH (K) (W) (x))$
28	27	eqeq1d	$⊢ (φ \land x \subseteq {Base}_{U}) \to (ocv (U) (ocv (U) (x)) = x \leftrightarrow ocH (K) (W) (ocH (K) (W) (x)) = x)$
29	21 28	bitrid	$⊢ (φ \land x \subseteq {Base}_{U}) \to (x = ocv (U) (ocv (U) (x)) \leftrightarrow ocH (K) (W) (ocH (K) (W) (x)) = x)$
30	20 29	bitr4d	$⊢ (φ \land x \subseteq {Base}_{U}) \to (x \in ran I \leftrightarrow x = ocv (U) (ocv (U) (x)))$
31	12 30	sylan2	$⊢ (φ \land x \in C) \to (x \in ran I \leftrightarrow x = ocv (U) (ocv (U) (x)))$
32	10 31	mpbird	$⊢ (φ \land x \in C) \to x \in ran I$
33		simpr	$⊢ (φ \land x \in ran I) \to x \in ran I$
34	5	adantr	$⊢ (φ \land x \in ran I) \to (K \in HL \land W \in H)$
35	1 13 2 14	dihrnss	$⊢ ((K \in HL \land W \in H) \land x \in ran I) \to x \subseteq {Base}_{DVecH (K) (W)}$
36	5 35	sylan	$⊢ (φ \land x \in ran I) \to x \subseteq {Base}_{DVecH (K) (W)}$
37	1 13 3 34 14 15 7 36	hlhilocv	$⊢ (φ \land x \in ran I) \to ocv (U) (x) = ocH (K) (W) (x)$
38	37	fveq2d	$⊢ (φ \land x \in ran I) \to ocv (U) (ocv (U) (x)) = ocv (U) (ocH (K) (W) (x))$
39	34 36 24	syl2anc	$⊢ (φ \land x \in ran I) \to ocH (K) (W) (x) \subseteq {Base}_{DVecH (K) (W)}$
40	1 13 3 34 14 15 7 39	hlhilocv	$⊢ (φ \land x \in ran I) \to ocv (U) (ocH (K) (W) (x)) = ocH (K) (W) (ocH (K) (W) (x))$
41	38 40	eqtrd	$⊢ (φ \land x \in ran I) \to ocv (U) (ocv (U) (x)) = ocH (K) (W) (ocH (K) (W) (x))$
42	41	eqeq1d	$⊢ (φ \land x \in ran I) \to (ocv (U) (ocv (U) (x)) = x \leftrightarrow ocH (K) (W) (ocH (K) (W) (x)) = x)$
43	42	biimpar	$⊢ ((φ \land x \in ran I) \land ocH (K) (W) (ocH (K) (W) (x)) = x) \to ocv (U) (ocv (U) (x)) = x$
44	43	eqcomd	$⊢ ((φ \land x \in ran I) \land ocH (K) (W) (ocH (K) (W) (x)) = x) \to x = ocv (U) (ocv (U) (x))$
45	44	ex	$⊢ (φ \land x \in ran I) \to (ocH (K) (W) (ocH (K) (W) (x)) = x \to x = ocv (U) (ocv (U) (x)))$
46	1 2 13 14 15 34 36	dochoccl	$⊢ (φ \land x \in ran I) \to (x \in ran I \leftrightarrow ocH (K) (W) (ocH (K) (W) (x)) = x)$
47	6 8	mp1i	$⊢ (φ \land x \in ran I) \to (x \in C \leftrightarrow x = ocv (U) (ocv (U) (x)))$
48	45 46 47	3imtr4d	$⊢ (φ \land x \in ran I) \to (x \in ran I \to x \in C)$
49	33 48	mpd	$⊢ (φ \land x \in ran I) \to x \in C$
50	32 49	impbida	$⊢ φ \to (x \in C \leftrightarrow x \in ran I)$
51	50	eqrdv	$⊢ φ \to C = ran I$

Metamath Proof Explorer

Theorem hlhillcs

Proof