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

Metamath Proof Explorer

Theorem dvhgrp

Proof