Step |
Hyp |
Ref |
Expression |
1 |
|
lsmub1.p |
|- .(+) = ( LSSum ` G ) |
2 |
|
eqid |
|- ( Base ` G ) = ( Base ` G ) |
3 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
4 |
2 3 1
|
lsmval |
|- ( ( U e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> ( U .(+) U ) = ran ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) ) |
5 |
4
|
anidms |
|- ( U e. ( SubGrp ` G ) -> ( U .(+) U ) = ran ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) ) |
6 |
3
|
subgcl |
|- ( ( U e. ( SubGrp ` G ) /\ x e. U /\ y e. U ) -> ( x ( +g ` G ) y ) e. U ) |
7 |
6
|
3expb |
|- ( ( U e. ( SubGrp ` G ) /\ ( x e. U /\ y e. U ) ) -> ( x ( +g ` G ) y ) e. U ) |
8 |
7
|
ralrimivva |
|- ( U e. ( SubGrp ` G ) -> A. x e. U A. y e. U ( x ( +g ` G ) y ) e. U ) |
9 |
|
eqid |
|- ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) = ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) |
10 |
9
|
fmpo |
|- ( A. x e. U A. y e. U ( x ( +g ` G ) y ) e. U <-> ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) : ( U X. U ) --> U ) |
11 |
8 10
|
sylib |
|- ( U e. ( SubGrp ` G ) -> ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) : ( U X. U ) --> U ) |
12 |
11
|
frnd |
|- ( U e. ( SubGrp ` G ) -> ran ( x e. U , y e. U |-> ( x ( +g ` G ) y ) ) C_ U ) |
13 |
5 12
|
eqsstrd |
|- ( U e. ( SubGrp ` G ) -> ( U .(+) U ) C_ U ) |
14 |
1
|
lsmub1 |
|- ( ( U e. ( SubGrp ` G ) /\ U e. ( SubGrp ` G ) ) -> U C_ ( U .(+) U ) ) |
15 |
14
|
anidms |
|- ( U e. ( SubGrp ` G ) -> U C_ ( U .(+) U ) ) |
16 |
13 15
|
eqssd |
|- ( U e. ( SubGrp ` G ) -> ( U .(+) U ) = U ) |