Metamath Proof Explorer


Theorem tgrpgrplem

Description: Lemma for tgrpgrp . (Contributed by NM, 6-Jun-2013)

Ref Expression
Hypotheses tgrpset.h 𝐻 = ( LHyp ‘ 𝐾 )
tgrpset.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
tgrpset.g 𝐺 = ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 )
tgrp.o + = ( +g𝐺 )
tgrp.b 𝐵 = ( Base ‘ 𝐾 )
Assertion tgrpgrplem ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐺 ∈ Grp )

Proof

Step Hyp Ref Expression
1 tgrpset.h 𝐻 = ( LHyp ‘ 𝐾 )
2 tgrpset.t 𝑇 = ( ( LTrn ‘ 𝐾 ) ‘ 𝑊 )
3 tgrpset.g 𝐺 = ( ( TGrp ‘ 𝐾 ) ‘ 𝑊 )
4 tgrp.o + = ( +g𝐺 )
5 tgrp.b 𝐵 = ( Base ‘ 𝐾 )
6 eqid ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
7 1 2 3 6 tgrpbase ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( Base ‘ 𝐺 ) = 𝑇 )
8 7 eqcomd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝑇 = ( Base ‘ 𝐺 ) )
9 4 a1i ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → + = ( +g𝐺 ) )
10 1 2 3 4 tgrpov ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ∧ ( 𝑥𝑇𝑦𝑇 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥𝑦 ) )
11 10 3expa ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥𝑦 ) )
12 11 3impb ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇𝑦𝑇 ) → ( 𝑥 + 𝑦 ) = ( 𝑥𝑦 ) )
13 1 2 ltrnco ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇𝑦𝑇 ) → ( 𝑥𝑦 ) ∈ 𝑇 )
14 12 13 eqeltrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇𝑦𝑇 ) → ( 𝑥 + 𝑦 ) ∈ 𝑇 )
15 coass ( ( 𝑥𝑦 ) ∘ 𝑧 ) = ( 𝑥 ∘ ( 𝑦𝑧 ) )
16 simpll ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → 𝐾 ∈ HL )
17 simplr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → 𝑊𝐻 )
18 simpr1 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → 𝑥𝑇 )
19 simpr2 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → 𝑦𝑇 )
20 16 17 18 19 10 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → ( 𝑥 + 𝑦 ) = ( 𝑥𝑦 ) )
21 20 oveq1d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( ( 𝑥𝑦 ) + 𝑧 ) )
22 simpl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) )
23 22 18 19 13 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → ( 𝑥𝑦 ) ∈ 𝑇 )
24 simpr3 ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → 𝑧𝑇 )
25 1 2 3 4 tgrpov ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ∧ ( ( 𝑥𝑦 ) ∈ 𝑇𝑧𝑇 ) ) → ( ( 𝑥𝑦 ) + 𝑧 ) = ( ( 𝑥𝑦 ) ∘ 𝑧 ) )
26 16 17 23 24 25 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → ( ( 𝑥𝑦 ) + 𝑧 ) = ( ( 𝑥𝑦 ) ∘ 𝑧 ) )
27 21 26 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( ( 𝑥𝑦 ) ∘ 𝑧 ) )
28 1 2 3 4 tgrpov ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ∧ ( 𝑦𝑇𝑧𝑇 ) ) → ( 𝑦 + 𝑧 ) = ( 𝑦𝑧 ) )
29 16 17 19 24 28 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → ( 𝑦 + 𝑧 ) = ( 𝑦𝑧 ) )
30 29 oveq2d ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → ( 𝑥 + ( 𝑦 + 𝑧 ) ) = ( 𝑥 + ( 𝑦𝑧 ) ) )
31 1 2 ltrnco ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑦𝑇𝑧𝑇 ) → ( 𝑦𝑧 ) ∈ 𝑇 )
32 22 19 24 31 syl3anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → ( 𝑦𝑧 ) ∈ 𝑇 )
33 1 2 3 4 tgrpov ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ∧ ( 𝑥𝑇 ∧ ( 𝑦𝑧 ) ∈ 𝑇 ) ) → ( 𝑥 + ( 𝑦𝑧 ) ) = ( 𝑥 ∘ ( 𝑦𝑧 ) ) )
34 16 17 18 32 33 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → ( 𝑥 + ( 𝑦𝑧 ) ) = ( 𝑥 ∘ ( 𝑦𝑧 ) ) )
35 30 34 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → ( 𝑥 + ( 𝑦 + 𝑧 ) ) = ( 𝑥 ∘ ( 𝑦𝑧 ) ) )
36 15 27 35 3eqtr4a ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ ( 𝑥𝑇𝑦𝑇𝑧𝑇 ) ) → ( ( 𝑥 + 𝑦 ) + 𝑧 ) = ( 𝑥 + ( 𝑦 + 𝑧 ) ) )
37 5 1 2 idltrn ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
38 simpll ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇 ) → 𝐾 ∈ HL )
39 simplr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇 ) → 𝑊𝐻 )
40 37 adantr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇 ) → ( I ↾ 𝐵 ) ∈ 𝑇 )
41 simpr ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇 ) → 𝑥𝑇 )
42 1 2 3 4 tgrpov ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ∧ ( ( I ↾ 𝐵 ) ∈ 𝑇𝑥𝑇 ) ) → ( ( I ↾ 𝐵 ) + 𝑥 ) = ( ( I ↾ 𝐵 ) ∘ 𝑥 ) )
43 38 39 40 41 42 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇 ) → ( ( I ↾ 𝐵 ) + 𝑥 ) = ( ( I ↾ 𝐵 ) ∘ 𝑥 ) )
44 5 1 2 ltrn1o ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇 ) → 𝑥 : 𝐵1-1-onto𝐵 )
45 f1of ( 𝑥 : 𝐵1-1-onto𝐵𝑥 : 𝐵𝐵 )
46 fcoi2 ( 𝑥 : 𝐵𝐵 → ( ( I ↾ 𝐵 ) ∘ 𝑥 ) = 𝑥 )
47 44 45 46 3syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇 ) → ( ( I ↾ 𝐵 ) ∘ 𝑥 ) = 𝑥 )
48 43 47 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇 ) → ( ( I ↾ 𝐵 ) + 𝑥 ) = 𝑥 )
49 1 2 ltrncnv ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇 ) → 𝑥𝑇 )
50 1 2 3 4 tgrpov ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ∧ ( 𝑥𝑇𝑥𝑇 ) ) → ( 𝑥 + 𝑥 ) = ( 𝑥𝑥 ) )
51 38 39 49 41 50 syl112anc ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇 ) → ( 𝑥 + 𝑥 ) = ( 𝑥𝑥 ) )
52 f1ococnv1 ( 𝑥 : 𝐵1-1-onto𝐵 → ( 𝑥𝑥 ) = ( I ↾ 𝐵 ) )
53 44 52 syl ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇 ) → ( 𝑥𝑥 ) = ( I ↾ 𝐵 ) )
54 51 53 eqtrd ( ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) ∧ 𝑥𝑇 ) → ( 𝑥 + 𝑥 ) = ( I ↾ 𝐵 ) )
55 8 9 14 36 37 48 49 54 isgrpd ( ( 𝐾 ∈ HL ∧ 𝑊𝐻 ) → 𝐺 ∈ Grp )