Metamath Proof Explorer

Theorem tgrpgrplem

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

Ref Expression
Hypotheses tgrpset.h 
|- H = ( LHyp ` K )
tgrpset.t 
|- T = ( ( LTrn ` K ) ` W )
tgrpset.g 
|- G = ( ( TGrp ` K ) ` W )
tgrp.o 
|- .+ = ( +g ` G )
tgrp.b 
|- B = ( Base ` K )
Assertion tgrpgrplem 
|- ( ( K e. HL /\ W e. H ) -> G e. 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 
 |-  .+ = ( +g ` G )
5 tgrp.b 
 |-  B = ( Base ` K )
6 eqid 
 |-  ( Base ` G ) = ( Base ` G )
7 1 2 3 6 tgrpbase 
 |-  ( ( K e. HL /\ W e. H ) -> ( Base ` G ) = T )
8 7 eqcomd 
 |-  ( ( K e. HL /\ W e. H ) -> T = ( Base ` G ) )
9 4 a1i 
 |-  ( ( K e. HL /\ W e. H ) -> .+ = ( +g ` G ) )
10 1 2 3 4 tgrpov 
 |-  ( ( K e. HL /\ W e. H /\ ( x e. T /\ y e. T ) ) -> ( x .+ y ) = ( x o. y ) )
11 10 3expa 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T ) ) -> ( x .+ y ) = ( x o. y ) )
12 11 3impb 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T /\ y e. T ) -> ( x .+ y ) = ( x o. y ) )
13 1 2 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T /\ y e. T ) -> ( x o. y ) e. T )
14 12 13 eqeltrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T /\ y e. T ) -> ( x .+ y ) e. T )
15 coass 
 |-  ( ( x o. y ) o. z ) = ( x o. ( y o. z ) )
16 simpll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> K e. HL )
17 simplr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> W e. H )
18 simpr1 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> x e. T )
19 simpr2 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> y e. T )
20 16 17 18 19 10 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> ( x .+ y ) = ( x o. y ) )
21 20 oveq1d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> ( ( x .+ y ) .+ z ) = ( ( x o. y ) .+ z ) )
22 simpl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> ( K e. HL /\ W e. H ) )
23 22 18 19 13 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> ( x o. y ) e. T )
24 simpr3 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> z e. T )
25 1 2 3 4 tgrpov 
 |-  ( ( K e. HL /\ W e. H /\ ( ( x o. y ) e. T /\ z e. T ) ) -> ( ( x o. y ) .+ z ) = ( ( x o. y ) o. z ) )
26 16 17 23 24 25 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> ( ( x o. y ) .+ z ) = ( ( x o. y ) o. z ) )
27 21 26 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> ( ( x .+ y ) .+ z ) = ( ( x o. y ) o. z ) )
28 1 2 3 4 tgrpov 
 |-  ( ( K e. HL /\ W e. H /\ ( y e. T /\ z e. T ) ) -> ( y .+ z ) = ( y o. z ) )
29 16 17 19 24 28 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> ( y .+ z ) = ( y o. z ) )
30 29 oveq2d 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> ( x .+ ( y .+ z ) ) = ( x .+ ( y o. z ) ) )
31 1 2 ltrnco 
 |-  ( ( ( K e. HL /\ W e. H ) /\ y e. T /\ z e. T ) -> ( y o. z ) e. T )
32 22 19 24 31 syl3anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> ( y o. z ) e. T )
33 1 2 3 4 tgrpov 
 |-  ( ( K e. HL /\ W e. H /\ ( x e. T /\ ( y o. z ) e. T ) ) -> ( x .+ ( y o. z ) ) = ( x o. ( y o. z ) ) )
34 16 17 18 32 33 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> ( x .+ ( y o. z ) ) = ( x o. ( y o. z ) ) )
35 30 34 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> ( x .+ ( y .+ z ) ) = ( x o. ( y o. z ) ) )
36 15 27 35 3eqtr4a 
 |-  ( ( ( K e. HL /\ W e. H ) /\ ( x e. T /\ y e. T /\ z e. T ) ) -> ( ( x .+ y ) .+ z ) = ( x .+ ( y .+ z ) ) )
37 5 1 2 idltrn 
 |-  ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. T )
38 simpll 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T ) -> K e. HL )
39 simplr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T ) -> W e. H )
40 37 adantr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T ) -> ( _I |` B ) e. T )
41 simpr 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T ) -> x e. T )
42 1 2 3 4 tgrpov 
 |-  ( ( K e. HL /\ W e. H /\ ( ( _I |` B ) e. T /\ x e. T ) ) -> ( ( _I |` B ) .+ x ) = ( ( _I |` B ) o. x ) )
43 38 39 40 41 42 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T ) -> ( ( _I |` B ) .+ x ) = ( ( _I |` B ) o. x ) )
44 5 1 2 ltrn1o 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T ) -> x : B -1-1-onto-> B )
45 f1of 
 |-  ( x : B -1-1-onto-> B -> x : B --> B )
46 fcoi2 
 |-  ( x : B --> B -> ( ( _I |` B ) o. x ) = x )
47 44 45 46 3syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T ) -> ( ( _I |` B ) o. x ) = x )
48 43 47 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T ) -> ( ( _I |` B ) .+ x ) = x )
49 1 2 ltrncnv 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T ) -> `' x e. T )
50 1 2 3 4 tgrpov 
 |-  ( ( K e. HL /\ W e. H /\ ( `' x e. T /\ x e. T ) ) -> ( `' x .+ x ) = ( `' x o. x ) )
51 38 39 49 41 50 syl112anc 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T ) -> ( `' x .+ x ) = ( `' x o. x ) )
52 f1ococnv1 
 |-  ( x : B -1-1-onto-> B -> ( `' x o. x ) = ( _I |` B ) )
53 44 52 syl 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T ) -> ( `' x o. x ) = ( _I |` B ) )
54 51 53 eqtrd 
 |-  ( ( ( K e. HL /\ W e. H ) /\ x e. T ) -> ( `' x .+ x ) = ( _I |` B ) )
55 8 9 14 36 37 48 49 54 isgrpd 
 |-  ( ( K e. HL /\ W e. H ) -> G e. Grp )