# 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 ) )`
` |-  ( ( 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 ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 )`