# Metamath Proof Explorer

## Theorem dvhgrp

Description: The full vector space U constructed from a Hilbert lattice K (given a fiducial hyperplane W ) is a group. (Contributed by NM, 19-Oct-2013) (Revised by Mario Carneiro, 24-Jun-2014)

Ref Expression
Hypotheses dvhgrp.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
dvhgrp.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
dvhgrp.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
dvhgrp.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
dvhgrp.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
dvhgrp.d ${⊢}{D}=\mathrm{Scalar}\left({U}\right)$
dvhgrp.p
dvhgrp.a
dvhgrp.o
dvhgrp.i ${⊢}{I}={inv}_{g}\left({D}\right)$
Assertion dvhgrp ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {U}\in \mathrm{Grp}$

### Proof

Step Hyp Ref Expression
1 dvhgrp.b ${⊢}{B}={\mathrm{Base}}_{{K}}$
2 dvhgrp.h ${⊢}{H}=\mathrm{LHyp}\left({K}\right)$
3 dvhgrp.t ${⊢}{T}=\mathrm{LTrn}\left({K}\right)\left({W}\right)$
4 dvhgrp.e ${⊢}{E}=\mathrm{TEndo}\left({K}\right)\left({W}\right)$
5 dvhgrp.u ${⊢}{U}=\mathrm{DVecH}\left({K}\right)\left({W}\right)$
6 dvhgrp.d ${⊢}{D}=\mathrm{Scalar}\left({U}\right)$
7 dvhgrp.p
8 dvhgrp.a
9 dvhgrp.o
10 dvhgrp.i ${⊢}{I}={inv}_{g}\left({D}\right)$
11 eqid ${⊢}{\mathrm{Base}}_{{U}}={\mathrm{Base}}_{{U}}$
12 2 3 4 5 11 dvhvbase ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{Base}}_{{U}}={T}×{E}$
13 12 eqcomd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {T}×{E}={\mathrm{Base}}_{{U}}$
14 8 a1i
15 2 3 4 5 6 7 8 dvhvaddcl
16 15 3impb
17 2 3 4 5 6 7 8 dvhvaddass
18 1 2 3 idltrn ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{I}↾}_{{B}}\in {T}$
19 eqid ${⊢}\mathrm{EDRing}\left({K}\right)\left({W}\right)=\mathrm{EDRing}\left({K}\right)\left({W}\right)$
20 2 19 5 6 dvhsca ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {D}=\mathrm{EDRing}\left({K}\right)\left({W}\right)$
21 2 19 erngdv ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to \mathrm{EDRing}\left({K}\right)\left({W}\right)\in \mathrm{DivRing}$
22 20 21 eqeltrd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {D}\in \mathrm{DivRing}$
23 drnggrp ${⊢}{D}\in \mathrm{DivRing}\to {D}\in \mathrm{Grp}$
24 22 23 syl ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {D}\in \mathrm{Grp}$
25 eqid ${⊢}{\mathrm{Base}}_{{D}}={\mathrm{Base}}_{{D}}$
26 25 9 grpidcl
27 24 26 syl
28 2 4 5 6 25 dvhbase ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {\mathrm{Base}}_{{D}}={E}$
29 27 28 eleqtrd
30 opelxpi
31 18 29 30 syl2anc
32 simpl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to \left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)$
33 18 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to {\mathrm{I}↾}_{{B}}\in {T}$
35 xp1st ${⊢}{f}\in \left({T}×{E}\right)\to {1}^{st}\left({f}\right)\in {T}$
36 35 adantl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to {1}^{st}\left({f}\right)\in {T}$
37 xp2nd ${⊢}{f}\in \left({T}×{E}\right)\to {2}^{nd}\left({f}\right)\in {E}$
38 37 adantl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to {2}^{nd}\left({f}\right)\in {E}$
39 2 3 4 5 6 8 7 dvhopvadd
40 32 33 34 36 38 39 syl122anc
41 1 2 3 ltrn1o ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {1}^{st}\left({f}\right)\in {T}\right)\to {1}^{st}\left({f}\right):{B}\underset{1-1 onto}{⟶}{B}$
42 36 41 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to {1}^{st}\left({f}\right):{B}\underset{1-1 onto}{⟶}{B}$
43 f1of ${⊢}{1}^{st}\left({f}\right):{B}\underset{1-1 onto}{⟶}{B}\to {1}^{st}\left({f}\right):{B}⟶{B}$
44 fcoi2 ${⊢}{1}^{st}\left({f}\right):{B}⟶{B}\to \left({\mathrm{I}↾}_{{B}}\right)\circ {1}^{st}\left({f}\right)={1}^{st}\left({f}\right)$
45 42 43 44 3syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to \left({\mathrm{I}↾}_{{B}}\right)\circ {1}^{st}\left({f}\right)={1}^{st}\left({f}\right)$
46 24 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to {D}\in \mathrm{Grp}$
47 28 adantr ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to {\mathrm{Base}}_{{D}}={E}$
48 38 47 eleqtrrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to {2}^{nd}\left({f}\right)\in {\mathrm{Base}}_{{D}}$
49 25 7 9 grplid
50 46 48 49 syl2anc
51 45 50 opeq12d
52 40 51 eqtrd
53 1st2nd2 ${⊢}{f}\in \left({T}×{E}\right)\to {f}=⟨{1}^{st}\left({f}\right),{2}^{nd}\left({f}\right)⟩$
54 53 adantl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to {f}=⟨{1}^{st}\left({f}\right),{2}^{nd}\left({f}\right)⟩$
55 54 oveq2d
56 52 55 54 3eqtr4d
57 2 3 ltrncnv ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {1}^{st}\left({f}\right)\in {T}\right)\to {{1}^{st}\left({f}\right)}^{-1}\in {T}$
58 36 57 syldan ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to {{1}^{st}\left({f}\right)}^{-1}\in {T}$
59 25 10 grpinvcl ${⊢}\left({D}\in \mathrm{Grp}\wedge {2}^{nd}\left({f}\right)\in {\mathrm{Base}}_{{D}}\right)\to {I}\left({2}^{nd}\left({f}\right)\right)\in {\mathrm{Base}}_{{D}}$
60 46 48 59 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to {I}\left({2}^{nd}\left({f}\right)\right)\in {\mathrm{Base}}_{{D}}$
61 60 47 eleqtrd ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to {I}\left({2}^{nd}\left({f}\right)\right)\in {E}$
62 opelxpi ${⊢}\left({{1}^{st}\left({f}\right)}^{-1}\in {T}\wedge {I}\left({2}^{nd}\left({f}\right)\right)\in {E}\right)\to ⟨{{1}^{st}\left({f}\right)}^{-1},{I}\left({2}^{nd}\left({f}\right)\right)⟩\in \left({T}×{E}\right)$
63 58 61 62 syl2anc ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to ⟨{{1}^{st}\left({f}\right)}^{-1},{I}\left({2}^{nd}\left({f}\right)\right)⟩\in \left({T}×{E}\right)$
64 54 oveq2d
65 2 3 4 5 6 8 7 dvhopvadd
66 32 58 61 36 38 65 syl122anc
67 f1ococnv1 ${⊢}{1}^{st}\left({f}\right):{B}\underset{1-1 onto}{⟶}{B}\to {{1}^{st}\left({f}\right)}^{-1}\circ {1}^{st}\left({f}\right)={\mathrm{I}↾}_{{B}}$
68 42 67 syl ${⊢}\left(\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\wedge {f}\in \left({T}×{E}\right)\right)\to {{1}^{st}\left({f}\right)}^{-1}\circ {1}^{st}\left({f}\right)={\mathrm{I}↾}_{{B}}$
69 25 7 9 10 grplinv
70 46 48 69 syl2anc
71 68 70 opeq12d
72 66 71 eqtrd
73 64 72 eqtrd
74 13 14 16 17 31 56 63 73 isgrpd ${⊢}\left({K}\in \mathrm{HL}\wedge {W}\in {H}\right)\to {U}\in \mathrm{Grp}$