This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( Base ` K )
dvhgrp.h 
|- H = ( LHyp ` K )
dvhgrp.t 
|- T = ( ( LTrn ` K ) ` W )
dvhgrp.e 
|- E = ( ( TEndo ` K ) ` W )
dvhgrp.u 
|- U = ( ( DVecH ` K ) ` W )
dvhgrp.d 
|- D = ( Scalar ` U )
dvhgrp.p 
|- .+^ = ( +g ` D )
dvhgrp.a 
|- .+ = ( +g ` U )
dvhgrp.o 
|- .0. = ( 0g ` D )
dvhgrp.i 
|- I = ( invg ` D )
Assertion dvhgrp 
|- ( ( K e. HL /\ W e. H ) -> U e. Grp )

Proof

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