hlhilset

Description: The final Hilbert space constructed from a Hilbert lattice K and an arbitrary hyperplane W in K . (Contributed by NM, 21-Jun-2015) (Revised by Mario Carneiro, 28-Jun-2015)

	Ref	Expression
Hypotheses	hlhilset.h	$⊢ H = LHyp (K)$
	hlhilset.l	$⊢ L = HLHil (K) (W)$
	hlhilset.u	$⊢ U = DVecH (K) (W)$
	hlhilset.v	$⊢ V = {Base}_{U}$
	hlhilset.p	$⊢ \underset{˙}{+} = +_{U}$
	hlhilset.e	$⊢ E = EDRing (K) (W)$
	hlhilset.g	$⊢ G = HGMap (K) (W)$
	hlhilset.r	$⊢ R = E sSet ⟨*_{ndx}, G⟩$
	hlhilset.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
	hlhilset.s	$⊢ S = HDMap (K) (W)$
	hlhilset.i	$⊢ \underset{˙}{,} = (x \in V, y \in V ⟼ S (y) (x))$
	hlhilset.k	$⊢ φ \to (K \in HL \land W \in H)$
Assertion	hlhilset	$⊢ φ \to L = \{⟨{Base}_{ndx}, V⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$

Proof

Step	Hyp	Ref	Expression
1		hlhilset.h	$⊢ H = LHyp (K)$
2		hlhilset.l	$⊢ L = HLHil (K) (W)$
3		hlhilset.u	$⊢ U = DVecH (K) (W)$
4		hlhilset.v	$⊢ V = {Base}_{U}$
5		hlhilset.p	$⊢ \underset{˙}{+} = +_{U}$
6		hlhilset.e	$⊢ E = EDRing (K) (W)$
7		hlhilset.g	$⊢ G = HGMap (K) (W)$
8		hlhilset.r	$⊢ R = E sSet ⟨*_{ndx}, G⟩$
9		hlhilset.t	$⊢ \underset{˙}{\cdot} = \cdot_{U}$
10		hlhilset.s	$⊢ S = HDMap (K) (W)$
11		hlhilset.i	$⊢ \underset{˙}{,} = (x \in V, y \in V ⟼ S (y) (x))$
12		hlhilset.k	$⊢ φ \to (K \in HL \land W \in H)$
13		elex	$⊢ K \in HL \to K \in V$
14	13	adantr	$⊢ (K \in HL \land W \in H) \to K \in V$
15	12 14	syl	$⊢ φ \to K \in V$
16	1	fvexi	$⊢ H \in V$
17	16	mptex	$⊢ (w \in H ⟼ ⦋ K / k ⦌ ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\})) \in V$
18		nfcv	$⊢ \underline{Ⅎ} k K$
19		nfcv	$⊢ \underline{Ⅎ} k H$
20		nfcsb1v	$⊢ \underline{Ⅎ} k ⦋ K / k ⦌ ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\})$
21	19 20	nfmpt	$⊢ \underline{Ⅎ} k (w \in H ⟼ ⦋ K / k ⦌ ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\}))$
22		fveq2	$⊢ k = K \to LHyp (k) = LHyp (K)$
23	22 1	eqtr4di	$⊢ k = K \to LHyp (k) = H$
24		csbeq1a	$⊢ k = K \to ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\}) = ⦋ K / k ⦌ ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\})$
25	23 24	mpteq12dv	$⊢ k = K \to (w \in LHyp (k) ⟼ ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\})) = (w \in H ⟼ ⦋ K / k ⦌ ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\}))$
26		df-hlhil	$⊢ HLHil = (k \in V ⟼ (w \in LHyp (k) ⟼ ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\})))$
27	18 21 25 26	fvmptf	$⊢ (K \in V \land (w \in H ⟼ ⦋ K / k ⦌ ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\})) \in V) \to HLHil (K) = (w \in H ⟼ ⦋ K / k ⦌ ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\}))$
28	15 17 27	sylancl	$⊢ φ \to HLHil (K) = (w \in H ⟼ ⦋ K / k ⦌ ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\}))$
29	15	adantr	$⊢ (φ \land w = W) \to K \in V$
30		fvexd	$⊢ ((φ \land w = W) \land k = K) \to DVecH (k) (w) \in V$
31		fvexd	$⊢ (((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \to {Base}_{u} \in V$
32		id	$⊢ v = {Base}_{u} \to v = {Base}_{u}$
33		id	$⊢ u = DVecH (k) (w) \to u = DVecH (k) (w)$
34		simpr	$⊢ ((φ \land w = W) \land k = K) \to k = K$
35	34	fveq2d	$⊢ ((φ \land w = W) \land k = K) \to DVecH (k) = DVecH (K)$
36		simplr	$⊢ ((φ \land w = W) \land k = K) \to w = W$
37	35 36	fveq12d	$⊢ ((φ \land w = W) \land k = K) \to DVecH (k) (w) = DVecH (K) (W)$
38	37 3	eqtr4di	$⊢ ((φ \land w = W) \land k = K) \to DVecH (k) (w) = U$
39	33 38	sylan9eqr	$⊢ (((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \to u = U$
40	39	fveq2d	$⊢ (((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \to {Base}_{u} = {Base}_{U}$
41	40 4	eqtr4di	$⊢ (((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \to {Base}_{u} = V$
42	32 41	sylan9eqr	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to v = V$
43	42	opeq2d	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to ⟨{Base}_{ndx}, v⟩ = ⟨{Base}_{ndx}, V⟩$
44	39	adantr	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to u = U$
45	44	fveq2d	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to +_{u} = +_{U}$
46	45 5	eqtr4di	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to +_{u} = \underset{˙}{+}$
47	46	opeq2d	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to ⟨+_{ndx}, +_{u}⟩ = ⟨+_{ndx}, \underset{˙}{+}⟩$
48	34	fveq2d	$⊢ ((φ \land w = W) \land k = K) \to EDRing (k) = EDRing (K)$
49	48 36	fveq12d	$⊢ ((φ \land w = W) \land k = K) \to EDRing (k) (w) = EDRing (K) (W)$
50	49 6	eqtr4di	$⊢ ((φ \land w = W) \land k = K) \to EDRing (k) (w) = E$
51	34	fveq2d	$⊢ ((φ \land w = W) \land k = K) \to HGMap (k) = HGMap (K)$
52	51 36	fveq12d	$⊢ ((φ \land w = W) \land k = K) \to HGMap (k) (w) = HGMap (K) (W)$
53	52 7	eqtr4di	$⊢ ((φ \land w = W) \land k = K) \to HGMap (k) (w) = G$
54	53	opeq2d	$⊢ ((φ \land w = W) \land k = K) \to ⟨_{ndx}, HGMap (k) (w)⟩ = ⟨_{ndx}, G⟩$
55	50 54	oveq12d	$⊢ ((φ \land w = W) \land k = K) \to EDRing (k) (w) sSet ⟨_{ndx}, HGMap (k) (w)⟩ = E sSet ⟨_{ndx}, G⟩$
56	55 8	eqtr4di	$⊢ ((φ \land w = W) \land k = K) \to EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩ = R$
57	56	opeq2d	$⊢ ((φ \land w = W) \land k = K) \to ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩⟩ = ⟨Scalar (ndx), R⟩$
58	57	ad2antrr	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩⟩ = ⟨Scalar (ndx), R⟩$
59	43 47 58	tpeq123d	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to \{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩⟩\} = \{⟨{Base}_{ndx}, V⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), R⟩\}$
60	44	fveq2d	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to \cdot_{u} = \cdot_{U}$
61	60 9	eqtr4di	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to \cdot_{u} = \underset{˙}{\cdot}$
62	61	opeq2d	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to ⟨\cdot_{ndx}, \cdot_{u}⟩ = ⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩$
63	34	fveq2d	$⊢ ((φ \land w = W) \land k = K) \to HDMap (k) = HDMap (K)$
64	63 36	fveq12d	$⊢ ((φ \land w = W) \land k = K) \to HDMap (k) (w) = HDMap (K) (W)$
65	64 10	eqtr4di	$⊢ ((φ \land w = W) \land k = K) \to HDMap (k) (w) = S$
66	65	ad2antrr	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to HDMap (k) (w) = S$
67	66	fveq1d	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to HDMap (k) (w) (y) = S (y)$
68	67	fveq1d	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to HDMap (k) (w) (y) (x) = S (y) (x)$
69	42 42 68	mpoeq123dv	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x)) = (x \in V, y \in V ⟼ S (y) (x))$
70	69 11	eqtr4di	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x)) = \underset{˙}{,}$
71	70	opeq2d	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩ = ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩$
72	62 71	preq12d	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\} = \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$
73	59 72	uneq12d	$⊢ ((((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \land v = {Base}_{u}) \to \{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\} = \{⟨{Base}_{ndx}, V⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$
74	31 73	csbied	$⊢ (((φ \land w = W) \land k = K) \land u = DVecH (k) (w)) \to ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\}) = \{⟨{Base}_{ndx}, V⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$
75	30 74	csbied	$⊢ ((φ \land w = W) \land k = K) \to ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\}) = \{⟨{Base}_{ndx}, V⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$
76	29 75	csbied	$⊢ (φ \land w = W) \to ⦋ K / k ⦌ ⦋ DVecH (k) (w) / u ⦌ ⦋ {Base}_{u} / v ⦌ (\{⟨{Base}_{ndx}, v⟩, ⟨+_{ndx}, +_{u}⟩, ⟨Scalar (ndx), EDRing (k) (w) sSet ⟨*_{ndx}, HGMap (k) (w)⟩⟩\} \cup \{⟨\cdot_{ndx}, \cdot_{u}⟩, ⟨\cdot_{𝑖} (ndx), (x \in v, y \in v ⟼ HDMap (k) (w) (y) (x))⟩\}) = \{⟨{Base}_{ndx}, V⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$
77	12	simprd	$⊢ φ \to W \in H$
78		tpex	$⊢ \{⟨{Base}_{ndx}, V⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), R⟩\} \in V$
79		prex	$⊢ \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\} \in V$
80	78 79	unex	$⊢ \{⟨{Base}_{ndx}, V⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\} \in V$
81	80	a1i	$⊢ φ \to \{⟨{Base}_{ndx}, V⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\} \in V$
82	28 76 77 81	fvmptd	$⊢ φ \to HLHil (K) (W) = \{⟨{Base}_{ndx}, V⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$
83	2 82	syl5eq	$⊢ φ \to L = \{⟨{Base}_{ndx}, V⟩, ⟨+_{ndx}, \underset{˙}{+}⟩, ⟨Scalar (ndx), R⟩\} \cup \{⟨\cdot_{ndx}, \underset{˙}{\cdot}⟩, ⟨\cdot_{𝑖} (ndx), \underset{˙}{,}⟩\}$

Metamath Proof Explorer

Theorem hlhilset

Proof