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 )

Metamath Proof Explorer

Theorem dvhgrp

Proof