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 )