tgrpgrplem

	Ref	Expression
Hypotheses	tgrpset.h	$⊢ H = LHyp (K)$
	tgrpset.t	$⊢ T = LTrn (K) (W)$
	tgrpset.g	$⊢ G = TGrp (K) (W)$
	tgrp.o	$⊢ \underset{˙}{+} = +_{G}$
	tgrp.b	$⊢ B = {Base}_{K}$
Assertion	tgrpgrplem	$⊢ (K \in HL \land W \in H) \to G \in Grp$

Proof

Step	Hyp	Ref	Expression
1		tgrpset.h	$⊢ H = LHyp (K)$
2		tgrpset.t	$⊢ T = LTrn (K) (W)$
3		tgrpset.g	$⊢ G = TGrp (K) (W)$
4		tgrp.o	$⊢ \underset{˙}{+} = +_{G}$
5		tgrp.b	$⊢ B = {Base}_{K}$
6		eqid	$⊢ {Base}_{G} = {Base}_{G}$
7	1 2 3 6	tgrpbase	$⊢ (K \in HL \land W \in H) \to {Base}_{G} = T$
8	7	eqcomd	$⊢ (K \in HL \land W \in H) \to T = {Base}_{G}$
9	4	a1i	$⊢ (K \in HL \land W \in H) \to \underset{˙}{+} = +_{G}$
10	1 2 3 4	tgrpov	$⊢ (K \in HL \land W \in H \land (x \in T \land y \in T)) \to x \underset{˙}{+} y = x \circ y$
11	10	3expa	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T)) \to x \underset{˙}{+} y = x \circ y$
12	11	3impb	$⊢ ((K \in HL \land W \in H) \land x \in T \land y \in T) \to x \underset{˙}{+} y = x \circ y$
13	1 2	ltrnco	$⊢ ((K \in HL \land W \in H) \land x \in T \land y \in T) \to x \circ y \in T$
14	12 13	eqeltrd	$⊢ ((K \in HL \land W \in H) \land x \in T \land y \in T) \to x \underset{˙}{+} y \in T$
15		coass	$⊢ (x \circ y) \circ z = x \circ (y \circ z)$
16		simpll	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to K \in HL$
17		simplr	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to W \in H$
18		simpr1	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to x \in T$
19		simpr2	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to y \in T$
20	16 17 18 19 10	syl112anc	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to x \underset{˙}{+} y = x \circ y$
21	20	oveq1d	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = (x \circ y) \underset{˙}{+} z$
22		simpl	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to (K \in HL \land W \in H)$
23	22 18 19 13	syl3anc	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to x \circ y \in T$
24		simpr3	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to z \in T$
25	1 2 3 4	tgrpov	$⊢ (K \in HL \land W \in H \land (x \circ y \in T \land z \in T)) \to (x \circ y) \underset{˙}{+} z = (x \circ y) \circ z$
26	16 17 23 24 25	syl112anc	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to (x \circ y) \underset{˙}{+} z = (x \circ y) \circ z$
27	21 26	eqtrd	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = (x \circ y) \circ z$
28	1 2 3 4	tgrpov	$⊢ (K \in HL \land W \in H \land (y \in T \land z \in T)) \to y \underset{˙}{+} z = y \circ z$
29	16 17 19 24 28	syl112anc	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to y \underset{˙}{+} z = y \circ z$
30	29	oveq2d	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to x \underset{˙}{+} (y \underset{˙}{+} z) = x \underset{˙}{+} (y \circ z)$
31	1 2	ltrnco	$⊢ ((K \in HL \land W \in H) \land y \in T \land z \in T) \to y \circ z \in T$
32	22 19 24 31	syl3anc	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to y \circ z \in T$
33	1 2 3 4	tgrpov	$⊢ (K \in HL \land W \in H \land (x \in T \land y \circ z \in T)) \to x \underset{˙}{+} (y \circ z) = x \circ (y \circ z)$
34	16 17 18 32 33	syl112anc	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to x \underset{˙}{+} (y \circ z) = x \circ (y \circ z)$
35	30 34	eqtrd	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to x \underset{˙}{+} (y \underset{˙}{+} z) = x \circ (y \circ z)$
36	15 27 35	3eqtr4a	$⊢ ((K \in HL \land W \in H) \land (x \in T \land y \in T \land z \in T)) \to (x \underset{˙}{+} y) \underset{˙}{+} z = x \underset{˙}{+} (y \underset{˙}{+} z)$
37	5 1 2	idltrn	$⊢ (K \in HL \land W \in H) \to {I ↾}_{B} \in T$
38		simpll	$⊢ ((K \in HL \land W \in H) \land x \in T) \to K \in HL$
39		simplr	$⊢ ((K \in HL \land W \in H) \land x \in T) \to W \in H$
40	37	adantr	$⊢ ((K \in HL \land W \in H) \land x \in T) \to {I ↾}_{B} \in T$
41		simpr	$⊢ ((K \in HL \land W \in H) \land x \in T) \to x \in T$
42	1 2 3 4	tgrpov	$⊢ (K \in HL \land W \in H \land ({I ↾}_{B} \in T \land x \in T)) \to ({I ↾}_{B}) \underset{˙}{+} x = ({I ↾}_{B}) \circ x$
43	38 39 40 41 42	syl112anc	$⊢ ((K \in HL \land W \in H) \land x \in T) \to ({I ↾}_{B}) \underset{˙}{+} x = ({I ↾}_{B}) \circ x$
44	5 1 2	ltrn1o	$⊢ ((K \in HL \land W \in H) \land x \in T) \to x : B \underset{1-1 onto}{⟶} B$
45		f1of	$⊢ x : B \underset{1-1 onto}{⟶} B \to x : B ⟶ B$
46		fcoi2	$⊢ x : B ⟶ B \to ({I ↾}_{B}) \circ x = x$
47	44 45 46	3syl	$⊢ ((K \in HL \land W \in H) \land x \in T) \to ({I ↾}_{B}) \circ x = x$
48	43 47	eqtrd	$⊢ ((K \in HL \land W \in H) \land x \in T) \to ({I ↾}_{B}) \underset{˙}{+} x = x$
49	1 2	ltrncnv	$⊢ ((K \in HL \land W \in H) \land x \in T) \to x^{-1} \in T$
50	1 2 3 4	tgrpov	$⊢ (K \in HL \land W \in H \land (x^{-1} \in T \land x \in T)) \to x^{-1} \underset{˙}{+} x = x^{-1} \circ x$
51	38 39 49 41 50	syl112anc	$⊢ ((K \in HL \land W \in H) \land x \in T) \to x^{-1} \underset{˙}{+} x = x^{-1} \circ x$
52		f1ococnv1	$⊢ x : B \underset{1-1 onto}{⟶} B \to x^{-1} \circ x = {I ↾}_{B}$
53	44 52	syl	$⊢ ((K \in HL \land W \in H) \land x \in T) \to x^{-1} \circ x = {I ↾}_{B}$
54	51 53	eqtrd	$⊢ ((K \in HL \land W \in H) \land x \in T) \to x^{-1} \underset{˙}{+} x = {I ↾}_{B}$
55	8 9 14 36 37 48 49 54	isgrpd	$⊢ (K \in HL \land W \in H) \to G \in Grp$

Metamath Proof Explorer

Theorem tgrpgrplem

Proof