Metamath Proof Explorer


Theorem 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 + ˙ = + U
hlhilset.e E = EDRing K W
hlhilset.g G = HGMap K W
hlhilset.r R = E sSet * ndx G
hlhilset.t · ˙ = U
hlhilset.s S = HDMap K W
hlhilset.i , ˙ = x V , y V S y x
hlhilset.k φ K HL W H
Assertion hlhilset φ L = Base ndx V + ndx + ˙ Scalar ndx R ndx · ˙ 𝑖 ndx , ˙

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