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	⊢ 𝐵 = ( Base ‘ 𝐾 )
	dvhgrp.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
	dvhgrp.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
	dvhgrp.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
	dvhgrp.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
	dvhgrp.d	⊢ 𝐷 = ( Scalar ‘ 𝑈 )
	dvhgrp.p	⊢ ⨣ = ( +_g ‘ 𝐷 )
	dvhgrp.a	⊢ + = ( +_g ‘ 𝑈 )
	dvhgrp.o	⊢ 0 = ( 0_g ‘ 𝐷 )
	dvhgrp.i	⊢ 𝐼 = ( inv_g ‘ 𝐷 )
Assertion	dvhgrp	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ Grp )

Proof

Step	Hyp	Ref	Expression
1		dvhgrp.b	⊢ 𝐵 = ( Base ‘ 𝐾 )
2		dvhgrp.h	⊢ 𝐻 = ( LHyp ‘ 𝐾 )
3		dvhgrp.t	⊢ 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
4		dvhgrp.e	⊢ 𝐸 = ( ( TEndo ‘ 𝐾 ) ‘ 𝑊 )
5		dvhgrp.u	⊢ 𝑈 = ( ( DVecH ‘ 𝐾 ) ‘ 𝑊 )
6		dvhgrp.d	⊢ 𝐷 = ( Scalar ‘ 𝑈 )
7		dvhgrp.p	⊢ ⨣ = ( +_g ‘ 𝐷 )
8		dvhgrp.a	⊢ + = ( +_g ‘ 𝑈 )
9		dvhgrp.o	⊢ 0 = ( 0_g ‘ 𝐷 )
10		dvhgrp.i	⊢ 𝐼 = ( inv_g ‘ 𝐷 )
11		eqid	⊢ ( Base ‘ 𝑈 ) = ( Base ‘ 𝑈 )
12	2 3 4 5 11	dvhvbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝑈 ) = ( 𝑇 × 𝐸 ) )
13	12	eqcomd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( 𝑇 × 𝐸 ) = ( Base ‘ 𝑈 ) )
14	8	a1i	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → + = ( +_g ‘ 𝑈 ) )
15	2 3 4 5 6 7 8	dvhvaddcl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) ) → ( 𝑓 + 𝑔 ) ∈ ( 𝑇 × 𝐸 ) )
16	15	3impb	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝑓 + 𝑔 ) ∈ ( 𝑇 × 𝐸 ) )
17	2 3 4 5 6 7 8	dvhvaddass	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) ∧ 𝑔 ∈ ( 𝑇 × 𝐸 ) ∧ ℎ ∈ ( 𝑇 × 𝐸 ) ) ) → ( ( 𝑓 + 𝑔 ) + ℎ ) = ( 𝑓 + ( 𝑔 + ℎ ) ) )
18	1 2 3	idltrn	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
19		eqid	⊢ ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 )
20	2 19 5 6	dvhsca	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 = ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) )
21	2 19	erngdv	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( ( EDRing ‘ 𝐾 ) ‘ 𝑊 ) ∈ DivRing )
22	20 21	eqeltrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ DivRing )
23		drnggrp	⊢ ( 𝐷 ∈ DivRing → 𝐷 ∈ Grp )
24	22 23	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝐷 ∈ Grp )
25		eqid	⊢ ( Base ‘ 𝐷 ) = ( Base ‘ 𝐷 )
26	25 9	grpidcl	⊢ ( 𝐷 ∈ Grp → 0 ∈ ( Base ‘ 𝐷 ) )
27	24 26	syl	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ∈ ( Base ‘ 𝐷 ) )
28	2 4 5 6 25	dvhbase	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ( Base ‘ 𝐷 ) = 𝐸 )
29	27 28	eleqtrd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 0 ∈ 𝐸 )
30		opelxpi	⊢ ( ( ( I ↾ 𝐵 ) ∈ 𝑇 ∧ 0 ∈ 𝐸 ) → ⟨ ( I ↾ 𝐵 ) , 0 ⟩ ∈ ( 𝑇 × 𝐸 ) )
31	18 29 30	syl2anc	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → ⟨ ( I ↾ 𝐵 ) , 0 ⟩ ∈ ( 𝑇 × 𝐸 ) )
32		simpl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) )
33	18	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
34	29	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → 0 ∈ 𝐸 )
35		xp1st	⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) → ( 1^st ‘ 𝑓 ) ∈ 𝑇 )
36	35	adantl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( 1^st ‘ 𝑓 ) ∈ 𝑇 )
37		xp2nd	⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) → ( 2^nd ‘ 𝑓 ) ∈ 𝐸 )
38	37	adantl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( 2^nd ‘ 𝑓 ) ∈ 𝐸 )
39	2 3 4 5 6 8 7	dvhopvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ( I ↾ 𝐵 ) ∈ 𝑇 ∧ 0 ∈ 𝐸 ) ∧ ( ( 1^st ‘ 𝑓 ) ∈ 𝑇 ∧ ( 2^nd ‘ 𝑓 ) ∈ 𝐸 ) ) → ( ⟨ ( I ↾ 𝐵 ) , 0 ⟩ + ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) = ⟨ ( ( I ↾ 𝐵 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 0 ⨣ ( 2^nd ‘ 𝑓 ) ) ⟩ )
40	32 33 34 36 38 39	syl122anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( ⟨ ( I ↾ 𝐵 ) , 0 ⟩ + ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) = ⟨ ( ( I ↾ 𝐵 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 0 ⨣ ( 2^nd ‘ 𝑓 ) ) ⟩ )
41	1 2 3	ltrn1o	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 1^st ‘ 𝑓 ) ∈ 𝑇 ) → ( 1^st ‘ 𝑓 ) : 𝐵 –1-1-onto→ 𝐵 )
42	36 41	syldan	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( 1^st ‘ 𝑓 ) : 𝐵 –1-1-onto→ 𝐵 )
43		f1of	⊢ ( ( 1^st ‘ 𝑓 ) : 𝐵 –1-1-onto→ 𝐵 → ( 1^st ‘ 𝑓 ) : 𝐵 ⟶ 𝐵 )
44		fcoi2	⊢ ( ( 1^st ‘ 𝑓 ) : 𝐵 ⟶ 𝐵 → ( ( I ↾ 𝐵 ) ∘ ( 1^st ‘ 𝑓 ) ) = ( 1^st ‘ 𝑓 ) )
45	42 43 44	3syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( ( I ↾ 𝐵 ) ∘ ( 1^st ‘ 𝑓 ) ) = ( 1^st ‘ 𝑓 ) )
46	24	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → 𝐷 ∈ Grp )
47	28	adantr	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( Base ‘ 𝐷 ) = 𝐸 )
48	38 47	eleqtrrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( 2^nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) )
49	25 7 9	grplid	⊢ ( ( 𝐷 ∈ Grp ∧ ( 2^nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) → ( 0 ⨣ ( 2^nd ‘ 𝑓 ) ) = ( 2^nd ‘ 𝑓 ) )
50	46 48 49	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( 0 ⨣ ( 2^nd ‘ 𝑓 ) ) = ( 2^nd ‘ 𝑓 ) )
51	45 50	opeq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ⟨ ( ( I ↾ 𝐵 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( 0 ⨣ ( 2^nd ‘ 𝑓 ) ) ⟩ = ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ )
52	40 51	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( ⟨ ( I ↾ 𝐵 ) , 0 ⟩ + ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) = ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ )
53		1st2nd2	⊢ ( 𝑓 ∈ ( 𝑇 × 𝐸 ) → 𝑓 = ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ )
54	53	adantl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → 𝑓 = ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ )
55	54	oveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( ⟨ ( I ↾ 𝐵 ) , 0 ⟩ + 𝑓 ) = ( ⟨ ( I ↾ 𝐵 ) , 0 ⟩ + ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) )
56	52 55 54	3eqtr4d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( ⟨ ( I ↾ 𝐵 ) , 0 ⟩ + 𝑓 ) = 𝑓 )
57	2 3	ltrncnv	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( 1^st ‘ 𝑓 ) ∈ 𝑇 ) → ^◡ ( 1^st ‘ 𝑓 ) ∈ 𝑇 )
58	36 57	syldan	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ^◡ ( 1^st ‘ 𝑓 ) ∈ 𝑇 )
59	25 10	grpinvcl	⊢ ( ( 𝐷 ∈ Grp ∧ ( 2^nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) → ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ∈ ( Base ‘ 𝐷 ) )
60	46 48 59	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ∈ ( Base ‘ 𝐷 ) )
61	60 47	eleqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ∈ 𝐸 )
62		opelxpi	⊢ ( ( ^◡ ( 1^st ‘ 𝑓 ) ∈ 𝑇 ∧ ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ∈ 𝐸 ) → ⟨ ^◡ ( 1^st ‘ 𝑓 ) , ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⟩ ∈ ( 𝑇 × 𝐸 ) )
63	58 61 62	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ⟨ ^◡ ( 1^st ‘ 𝑓 ) , ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⟩ ∈ ( 𝑇 × 𝐸 ) )
64	54	oveq2d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( ⟨ ^◡ ( 1^st ‘ 𝑓 ) , ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⟩ + 𝑓 ) = ( ⟨ ^◡ ( 1^st ‘ 𝑓 ) , ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⟩ + ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) )
65	2 3 4 5 6 8 7	dvhopvadd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ ( ^◡ ( 1^st ‘ 𝑓 ) ∈ 𝑇 ∧ ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ∈ 𝐸 ) ∧ ( ( 1^st ‘ 𝑓 ) ∈ 𝑇 ∧ ( 2^nd ‘ 𝑓 ) ∈ 𝐸 ) ) → ( ⟨ ^◡ ( 1^st ‘ 𝑓 ) , ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⟩ + ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) = ⟨ ( ^◡ ( 1^st ‘ 𝑓 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⨣ ( 2^nd ‘ 𝑓 ) ) ⟩ )
66	32 58 61 36 38 65	syl122anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( ⟨ ^◡ ( 1^st ‘ 𝑓 ) , ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⟩ + ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) = ⟨ ( ^◡ ( 1^st ‘ 𝑓 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⨣ ( 2^nd ‘ 𝑓 ) ) ⟩ )
67		f1ococnv1	⊢ ( ( 1^st ‘ 𝑓 ) : 𝐵 –1-1-onto→ 𝐵 → ( ^◡ ( 1^st ‘ 𝑓 ) ∘ ( 1^st ‘ 𝑓 ) ) = ( I ↾ 𝐵 ) )
68	42 67	syl	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( ^◡ ( 1^st ‘ 𝑓 ) ∘ ( 1^st ‘ 𝑓 ) ) = ( I ↾ 𝐵 ) )
69	25 7 9 10	grplinv	⊢ ( ( 𝐷 ∈ Grp ∧ ( 2^nd ‘ 𝑓 ) ∈ ( Base ‘ 𝐷 ) ) → ( ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⨣ ( 2^nd ‘ 𝑓 ) ) = 0 )
70	46 48 69	syl2anc	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⨣ ( 2^nd ‘ 𝑓 ) ) = 0 )
71	68 70	opeq12d	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ⟨ ( ^◡ ( 1^st ‘ 𝑓 ) ∘ ( 1^st ‘ 𝑓 ) ) , ( ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⨣ ( 2^nd ‘ 𝑓 ) ) ⟩ = ⟨ ( I ↾ 𝐵 ) , 0 ⟩ )
72	66 71	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( ⟨ ^◡ ( 1^st ‘ 𝑓 ) , ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⟩ + ⟨ ( 1^st ‘ 𝑓 ) , ( 2^nd ‘ 𝑓 ) ⟩ ) = ⟨ ( I ↾ 𝐵 ) , 0 ⟩ )
73	64 72	eqtrd	⊢ ( ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) ∧ 𝑓 ∈ ( 𝑇 × 𝐸 ) ) → ( ⟨ ^◡ ( 1^st ‘ 𝑓 ) , ( 𝐼 ‘ ( 2^nd ‘ 𝑓 ) ) ⟩ + 𝑓 ) = ⟨ ( I ↾ 𝐵 ) , 0 ⟩ )
74	13 14 16 17 31 56 63 73	isgrpd	⊢ ( ( 𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻 ) → 𝑈 ∈ Grp )

Metamath Proof Explorer

Theorem dvhgrp

Proof