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 ) |