hlhilhillem

	Ref	Expression
Hypotheses	hlhilphl.h	$⊢ H = LHyp (K)$
	hlhilphllem.u	$⊢ U = HLHil (K) (W)$
	hlhilphl.k	$⊢ φ \to (K \in HL \land W \in H)$
	hlhilphllem.f	$⊢ F = Scalar (U)$
	hlhilphllem.l	$⊢ L = DVecH (K) (W)$
	hlhilphllem.v	$⊢ V = {Base}_{L}$
	hlhilphllem.a	$⊢ \underset{˙}{+} = +_{L}$
	hlhilphllem.s	$⊢ \underset{˙}{\cdot} = \cdot_{L}$
	hlhilphllem.r	$⊢ R = Scalar (L)$
	hlhilphllem.b	$⊢ B = {Base}_{R}$
	hlhilphllem.p	$⊢ \underset{˙}{⨣} = +_{R}$
	hlhilphllem.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
	hlhilphllem.q	$⊢ Q = 0_{R}$
	hlhilphllem.z	$⊢ \underset{˙}{0} = 0_{L}$
	hlhilphllem.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (U)$
	hlhilphllem.j	$⊢ J = HDMap (K) (W)$
	hlhilphllem.g	$⊢ G = HGMap (K) (W)$
	hlhilphllem.e	$⊢ E = (x \in V, y \in V ⟼ J (y) (x))$
	hlhilphllem.o	$⊢ O = ocv (U)$
	hlhilphllem.c	$⊢ C = ClSubSp (U)$
Assertion	hlhilhillem	$⊢ φ \to U \in Hil$

Proof

Step	Hyp	Ref	Expression
1		hlhilphl.h	$⊢ H = LHyp (K)$
2		hlhilphllem.u	$⊢ U = HLHil (K) (W)$
3		hlhilphl.k	$⊢ φ \to (K \in HL \land W \in H)$
4		hlhilphllem.f	$⊢ F = Scalar (U)$
5		hlhilphllem.l	$⊢ L = DVecH (K) (W)$
6		hlhilphllem.v	$⊢ V = {Base}_{L}$
7		hlhilphllem.a	$⊢ \underset{˙}{+} = +_{L}$
8		hlhilphllem.s	$⊢ \underset{˙}{\cdot} = \cdot_{L}$
9		hlhilphllem.r	$⊢ R = Scalar (L)$
10		hlhilphllem.b	$⊢ B = {Base}_{R}$
11		hlhilphllem.p	$⊢ \underset{˙}{⨣} = +_{R}$
12		hlhilphllem.t	$⊢ \underset{˙}{\times} = \cdot_{R}$
13		hlhilphllem.q	$⊢ Q = 0_{R}$
14		hlhilphllem.z	$⊢ \underset{˙}{0} = 0_{L}$
15		hlhilphllem.i	$⊢ \underset{˙}{,} = \cdot_{𝑖} (U)$
16		hlhilphllem.j	$⊢ J = HDMap (K) (W)$
17		hlhilphllem.g	$⊢ G = HGMap (K) (W)$
18		hlhilphllem.e	$⊢ E = (x \in V, y \in V ⟼ J (y) (x))$
19		hlhilphllem.o	$⊢ O = ocv (U)$
20		hlhilphllem.c	$⊢ C = ClSubSp (U)$
21	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18	hlhilphllem	$⊢ φ \to U \in PreHil$
22	3	adantr	$⊢ (φ \land x \in C) \to (K \in HL \land W \in H)$
23		eqid	$⊢ ocH (K) (W) = ocH (K) (W)$
24		eqid	$⊢ DIsoH (K) (W) = DIsoH (K) (W)$
25	1 24 2 20 3	hlhillcs	$⊢ φ \to C = ran DIsoH (K) (W)$
26	25	eleq2d	$⊢ φ \to (x \in C \leftrightarrow x \in ran DIsoH (K) (W))$
27	26	biimpa	$⊢ (φ \land x \in C) \to x \in ran DIsoH (K) (W)$
28	1 5 24 6	dihrnss	$⊢ ((K \in HL \land W \in H) \land x \in ran DIsoH (K) (W)) \to x \subseteq V$
29	3 28	sylan	$⊢ (φ \land x \in ran DIsoH (K) (W)) \to x \subseteq V$
30	27 29	syldan	$⊢ (φ \land x \in C) \to x \subseteq V$
31	1 5 2 22 6 23 19 30	hlhilocv	$⊢ (φ \land x \in C) \to O (x) = ocH (K) (W) (x)$
32	31	oveq2d	$⊢ (φ \land x \in C) \to x LSSum (L) O (x) = x LSSum (L) ocH (K) (W) (x)$
33		eqid	$⊢ LSSum (L) = LSSum (L)$
34	1 5 2 3 33	hlhillsm	$⊢ φ \to LSSum (L) = LSSum (U)$
35	34	adantr	$⊢ (φ \land x \in C) \to LSSum (L) = LSSum (U)$
36	35	oveqd	$⊢ (φ \land x \in C) \to x LSSum (L) O (x) = x LSSum (U) O (x)$
37		eqid	$⊢ LSubSp (L) = LSubSp (L)$
38	3	adantr	$⊢ (φ \land x \in ran DIsoH (K) (W)) \to (K \in HL \land W \in H)$
39	1 5 24 37	dihrnlss	$⊢ ((K \in HL \land W \in H) \land x \in ran DIsoH (K) (W)) \to x \in LSubSp (L)$
40	3 39	sylan	$⊢ (φ \land x \in ran DIsoH (K) (W)) \to x \in LSubSp (L)$
41	1 24 5 6 23 38 29	dochoccl	$⊢ (φ \land x \in ran DIsoH (K) (W)) \to (x \in ran DIsoH (K) (W) \leftrightarrow ocH (K) (W) (ocH (K) (W) (x)) = x)$
42	41	biimpd	$⊢ (φ \land x \in ran DIsoH (K) (W)) \to (x \in ran DIsoH (K) (W) \to ocH (K) (W) (ocH (K) (W) (x)) = x)$
43	42	ex	$⊢ φ \to (x \in ran DIsoH (K) (W) \to (x \in ran DIsoH (K) (W) \to ocH (K) (W) (ocH (K) (W) (x)) = x))$
44	43	pm2.43d	$⊢ φ \to (x \in ran DIsoH (K) (W) \to ocH (K) (W) (ocH (K) (W) (x)) = x)$
45	44	imp	$⊢ (φ \land x \in ran DIsoH (K) (W)) \to ocH (K) (W) (ocH (K) (W) (x)) = x$
46	1 23 5 6 37 33 38 40 45	dochexmid	$⊢ (φ \land x \in ran DIsoH (K) (W)) \to x LSSum (L) ocH (K) (W) (x) = V$
47	27 46	syldan	$⊢ (φ \land x \in C) \to x LSSum (L) ocH (K) (W) (x) = V$
48	32 36 47	3eqtr3d	$⊢ (φ \land x \in C) \to x LSSum (U) O (x) = V$
49	1 2 3 5 6	hlhilbase	$⊢ φ \to V = {Base}_{U}$
50	49	adantr	$⊢ (φ \land x \in C) \to V = {Base}_{U}$
51	48 50	eqtrd	$⊢ (φ \land x \in C) \to x LSSum (U) O (x) = {Base}_{U}$
52	51	ralrimiva	$⊢ φ \to \forall x \in C x LSSum (U) O (x) = {Base}_{U}$
53		eqid	$⊢ {Base}_{U} = {Base}_{U}$
54		eqid	$⊢ LSSum (U) = LSSum (U)$
55	53 54 19 20	ishil2	$⊢ U \in Hil \leftrightarrow (U \in PreHil \land \forall x \in C x LSSum (U) O (x) = {Base}_{U})$
56	21 52 55	sylanbrc	$⊢ φ \to U \in Hil$

Metamath Proof Explorer

Theorem hlhilhillem

Proof