Metamath Proof Explorer

Theorem hhssabloilem

Description: Lemma for hhssabloi . Formerly part of proof for hhssabloi which was based on the deprecated definition "SubGrpOp" for subgroups. (Contributed by NM, 9-Apr-2008) (Revised by Mario Carneiro, 23-Dec-2013) (Revised by AV, 27-Aug-2021) (New usage is discouraged.)

Ref Expression
Hypothesis hhssabl.1 
|- H e. SH
Assertion hhssabloilem 
|- ( +h e. GrpOp /\ ( +h |` ( H X. H ) ) e. GrpOp /\ ( +h |` ( H X. H ) ) C_ +h )

Proof

Step Hyp Ref Expression
1 hhssabl.1 
 |-  H e. SH
2 hilablo 
 |-  +h e. AbelOp
3 ablogrpo 
 |-  ( +h e. AbelOp -> +h e. GrpOp )
4 2 3 ax-mp 
 |-  +h e. GrpOp
5 1 elexi 
 |-  H e. _V
6 eqid 
 |-  ran +h = ran +h
7 6 grpofo 
 |-  ( +h e. GrpOp -> +h : ( ran +h X. ran +h ) -onto-> ran +h )
8 fof 
 |-  ( +h : ( ran +h X. ran +h ) -onto-> ran +h -> +h : ( ran +h X. ran +h ) --> ran +h )
9 4 7 8 mp2b 
 |-  +h : ( ran +h X. ran +h ) --> ran +h
10 1 shssii 
 |-  H C_ ~H
11 df-hba 
 |-  ~H = ( BaseSet ` <. <. +h , .h >. , normh >. )
12 eqid 
 |-  <. <. +h , .h >. , normh >. = <. <. +h , .h >. , normh >.
13 12 hhva 
 |-  +h = ( +v ` <. <. +h , .h >. , normh >. )
14 11 13 bafval 
 |-  ~H = ran +h
15 10 14 sseqtri 
 |-  H C_ ran +h
16 xpss12 
 |-  ( ( H C_ ran +h /\ H C_ ran +h ) -> ( H X. H ) C_ ( ran +h X. ran +h ) )
17 15 15 16 mp2an 
 |-  ( H X. H ) C_ ( ran +h X. ran +h )
18 fssres 
 |-  ( ( +h : ( ran +h X. ran +h ) --> ran +h /\ ( H X. H ) C_ ( ran +h X. ran +h ) ) -> ( +h |` ( H X. H ) ) : ( H X. H ) --> ran +h )
19 9 17 18 mp2an 
 |-  ( +h |` ( H X. H ) ) : ( H X. H ) --> ran +h
20 ffn 
 |-  ( ( +h |` ( H X. H ) ) : ( H X. H ) --> ran +h -> ( +h |` ( H X. H ) ) Fn ( H X. H ) )
21 19 20 ax-mp 
 |-  ( +h |` ( H X. H ) ) Fn ( H X. H )
22 ovres 
 |-  ( ( x e. H /\ y e. H ) -> ( x ( +h |` ( H X. H ) ) y ) = ( x +h y ) )
23 shaddcl 
 |-  ( ( H e. SH /\ x e. H /\ y e. H ) -> ( x +h y ) e. H )
24 1 23 mp3an1 
 |-  ( ( x e. H /\ y e. H ) -> ( x +h y ) e. H )
25 22 24 eqeltrd 
 |-  ( ( x e. H /\ y e. H ) -> ( x ( +h |` ( H X. H ) ) y ) e. H )
26 25 rgen2 
 |-  A. x e. H A. y e. H ( x ( +h |` ( H X. H ) ) y ) e. H
27 ffnov 
 |-  ( ( +h |` ( H X. H ) ) : ( H X. H ) --> H <-> ( ( +h |` ( H X. H ) ) Fn ( H X. H ) /\ A. x e. H A. y e. H ( x ( +h |` ( H X. H ) ) y ) e. H ) )
28 21 26 27 mpbir2an 
 |-  ( +h |` ( H X. H ) ) : ( H X. H ) --> H
29 22 oveq1d 
 |-  ( ( x e. H /\ y e. H ) -> ( ( x ( +h |` ( H X. H ) ) y ) +h z ) = ( ( x +h y ) +h z ) )
30 29 3adant3 
 |-  ( ( x e. H /\ y e. H /\ z e. H ) -> ( ( x ( +h |` ( H X. H ) ) y ) +h z ) = ( ( x +h y ) +h z ) )
31 ovres 
 |-  ( ( ( x ( +h |` ( H X. H ) ) y ) e. H /\ z e. H ) -> ( ( x ( +h |` ( H X. H ) ) y ) ( +h |` ( H X. H ) ) z ) = ( ( x ( +h |` ( H X. H ) ) y ) +h z ) )
32 25 31 stoic3 
 |-  ( ( x e. H /\ y e. H /\ z e. H ) -> ( ( x ( +h |` ( H X. H ) ) y ) ( +h |` ( H X. H ) ) z ) = ( ( x ( +h |` ( H X. H ) ) y ) +h z ) )
33 ovres 
 |-  ( ( y e. H /\ z e. H ) -> ( y ( +h |` ( H X. H ) ) z ) = ( y +h z ) )
34 33 oveq2d 
 |-  ( ( y e. H /\ z e. H ) -> ( x +h ( y ( +h |` ( H X. H ) ) z ) ) = ( x +h ( y +h z ) ) )
35 34 3adant1 
 |-  ( ( x e. H /\ y e. H /\ z e. H ) -> ( x +h ( y ( +h |` ( H X. H ) ) z ) ) = ( x +h ( y +h z ) ) )
36 28 fovcl 
 |-  ( ( y e. H /\ z e. H ) -> ( y ( +h |` ( H X. H ) ) z ) e. H )
37 ovres 
 |-  ( ( x e. H /\ ( y ( +h |` ( H X. H ) ) z ) e. H ) -> ( x ( +h |` ( H X. H ) ) ( y ( +h |` ( H X. H ) ) z ) ) = ( x +h ( y ( +h |` ( H X. H ) ) z ) ) )
38 36 37 sylan2 
 |-  ( ( x e. H /\ ( y e. H /\ z e. H ) ) -> ( x ( +h |` ( H X. H ) ) ( y ( +h |` ( H X. H ) ) z ) ) = ( x +h ( y ( +h |` ( H X. H ) ) z ) ) )
39 38 3impb 
 |-  ( ( x e. H /\ y e. H /\ z e. H ) -> ( x ( +h |` ( H X. H ) ) ( y ( +h |` ( H X. H ) ) z ) ) = ( x +h ( y ( +h |` ( H X. H ) ) z ) ) )
40 15 sseli 
 |-  ( x e. H -> x e. ran +h )
41 15 sseli 
 |-  ( y e. H -> y e. ran +h )
42 15 sseli 
 |-  ( z e. H -> z e. ran +h )
43 6 grpoass 
 |-  ( ( +h e. GrpOp /\ ( x e. ran +h /\ y e. ran +h /\ z e. ran +h ) ) -> ( ( x +h y ) +h z ) = ( x +h ( y +h z ) ) )
44 4 43 mpan 
 |-  ( ( x e. ran +h /\ y e. ran +h /\ z e. ran +h ) -> ( ( x +h y ) +h z ) = ( x +h ( y +h z ) ) )
45 40 41 42 44 syl3an 
 |-  ( ( x e. H /\ y e. H /\ z e. H ) -> ( ( x +h y ) +h z ) = ( x +h ( y +h z ) ) )
46 35 39 45 3eqtr4d 
 |-  ( ( x e. H /\ y e. H /\ z e. H ) -> ( x ( +h |` ( H X. H ) ) ( y ( +h |` ( H X. H ) ) z ) ) = ( ( x +h y ) +h z ) )
47 30 32 46 3eqtr4d 
 |-  ( ( x e. H /\ y e. H /\ z e. H ) -> ( ( x ( +h |` ( H X. H ) ) y ) ( +h |` ( H X. H ) ) z ) = ( x ( +h |` ( H X. H ) ) ( y ( +h |` ( H X. H ) ) z ) ) )
48 hilid 
 |-  ( GId ` +h ) = 0h
49 sh0 
 |-  ( H e. SH -> 0h e. H )
50 1 49 ax-mp 
 |-  0h e. H
51 48 50 eqeltri 
 |-  ( GId ` +h ) e. H
52 ovres 
 |-  ( ( ( GId ` +h ) e. H /\ x e. H ) -> ( ( GId ` +h ) ( +h |` ( H X. H ) ) x ) = ( ( GId ` +h ) +h x ) )
53 51 52 mpan 
 |-  ( x e. H -> ( ( GId ` +h ) ( +h |` ( H X. H ) ) x ) = ( ( GId ` +h ) +h x ) )
54 eqid 
 |-  ( GId ` +h ) = ( GId ` +h )
55 6 54 grpolid 
 |-  ( ( +h e. GrpOp /\ x e. ran +h ) -> ( ( GId ` +h ) +h x ) = x )
56 4 40 55 sylancr 
 |-  ( x e. H -> ( ( GId ` +h ) +h x ) = x )
57 53 56 eqtrd 
 |-  ( x e. H -> ( ( GId ` +h ) ( +h |` ( H X. H ) ) x ) = x )
58 12 hhnv 
 |-  <. <. +h , .h >. , normh >. e. NrmCVec
59 12 hhsm 
 |-  .h = ( .sOLD ` <. <. +h , .h >. , normh >. )
60 eqid 
 |-  ( .h o. `' ( 2nd |` ( { -u 1 } X. _V ) ) ) = ( .h o. `' ( 2nd |` ( { -u 1 } X. _V ) ) )
61 13 59 60 nvinvfval 
 |-  ( <. <. +h , .h >. , normh >. e. NrmCVec -> ( .h o. `' ( 2nd |` ( { -u 1 } X. _V ) ) ) = ( inv ` +h ) )
62 58 61 ax-mp 
 |-  ( .h o. `' ( 2nd |` ( { -u 1 } X. _V ) ) ) = ( inv ` +h )
63 62 eqcomi 
 |-  ( inv ` +h ) = ( .h o. `' ( 2nd |` ( { -u 1 } X. _V ) ) )
64 63 fveq1i 
 |-  ( ( inv ` +h ) ` x ) = ( ( .h o. `' ( 2nd |` ( { -u 1 } X. _V ) ) ) ` x )
65 ax-hfvmul 
 |-  .h : ( CC X. ~H ) --> ~H
66 ffn 
 |-  ( .h : ( CC X. ~H ) --> ~H -> .h Fn ( CC X. ~H ) )
67 65 66 ax-mp 
 |-  .h Fn ( CC X. ~H )
68 neg1cn 
 |-  -u 1 e. CC
69 60 curry1val 
 |-  ( ( .h Fn ( CC X. ~H ) /\ -u 1 e. CC ) -> ( ( .h o. `' ( 2nd |` ( { -u 1 } X. _V ) ) ) ` x ) = ( -u 1 .h x ) )
70 67 68 69 mp2an 
 |-  ( ( .h o. `' ( 2nd |` ( { -u 1 } X. _V ) ) ) ` x ) = ( -u 1 .h x )
71 shmulcl 
 |-  ( ( H e. SH /\ -u 1 e. CC /\ x e. H ) -> ( -u 1 .h x ) e. H )
72 1 68 71 mp3an12 
 |-  ( x e. H -> ( -u 1 .h x ) e. H )
73 70 72 eqeltrid 
 |-  ( x e. H -> ( ( .h o. `' ( 2nd |` ( { -u 1 } X. _V ) ) ) ` x ) e. H )
74 64 73 eqeltrid 
 |-  ( x e. H -> ( ( inv ` +h ) ` x ) e. H )
75 ovres 
 |-  ( ( ( ( inv ` +h ) ` x ) e. H /\ x e. H ) -> ( ( ( inv ` +h ) ` x ) ( +h |` ( H X. H ) ) x ) = ( ( ( inv ` +h ) ` x ) +h x ) )
76 74 75 mpancom 
 |-  ( x e. H -> ( ( ( inv ` +h ) ` x ) ( +h |` ( H X. H ) ) x ) = ( ( ( inv ` +h ) ` x ) +h x ) )
77 eqid 
 |-  ( inv ` +h ) = ( inv ` +h )
78 6 54 77 grpolinv 
 |-  ( ( +h e. GrpOp /\ x e. ran +h ) -> ( ( ( inv ` +h ) ` x ) +h x ) = ( GId ` +h ) )
79 4 40 78 sylancr 
 |-  ( x e. H -> ( ( ( inv ` +h ) ` x ) +h x ) = ( GId ` +h ) )
80 76 79 eqtrd 
 |-  ( x e. H -> ( ( ( inv ` +h ) ` x ) ( +h |` ( H X. H ) ) x ) = ( GId ` +h ) )
81 5 28 47 51 57 74 80 isgrpoi 
 |-  ( +h |` ( H X. H ) ) e. GrpOp
82 resss 
 |-  ( +h |` ( H X. H ) ) C_ +h
83 4 81 82 3pm3.2i 
 |-  ( +h e. GrpOp /\ ( +h |` ( H X. H ) ) e. GrpOp /\ ( +h |` ( H X. H ) ) C_ +h )