Step |
Hyp |
Ref |
Expression |
1 |
|
lagsubg.1 |
|- X = ( Base ` G ) |
2 |
|
simpr |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> X e. Fin ) |
3 |
|
pwfi |
|- ( X e. Fin <-> ~P X e. Fin ) |
4 |
2 3
|
sylib |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ~P X e. Fin ) |
5 |
|
eqid |
|- ( G ~QG Y ) = ( G ~QG Y ) |
6 |
1 5
|
eqger |
|- ( Y e. ( SubGrp ` G ) -> ( G ~QG Y ) Er X ) |
7 |
6
|
adantr |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( G ~QG Y ) Er X ) |
8 |
7
|
qsss |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( X /. ( G ~QG Y ) ) C_ ~P X ) |
9 |
4 8
|
ssfid |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( X /. ( G ~QG Y ) ) e. Fin ) |
10 |
|
hashcl |
|- ( ( X /. ( G ~QG Y ) ) e. Fin -> ( # ` ( X /. ( G ~QG Y ) ) ) e. NN0 ) |
11 |
9 10
|
syl |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` ( X /. ( G ~QG Y ) ) ) e. NN0 ) |
12 |
11
|
nn0zd |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` ( X /. ( G ~QG Y ) ) ) e. ZZ ) |
13 |
|
id |
|- ( X e. Fin -> X e. Fin ) |
14 |
1
|
subgss |
|- ( Y e. ( SubGrp ` G ) -> Y C_ X ) |
15 |
|
ssfi |
|- ( ( X e. Fin /\ Y C_ X ) -> Y e. Fin ) |
16 |
13 14 15
|
syl2anr |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> Y e. Fin ) |
17 |
|
hashcl |
|- ( Y e. Fin -> ( # ` Y ) e. NN0 ) |
18 |
16 17
|
syl |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` Y ) e. NN0 ) |
19 |
18
|
nn0zd |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` Y ) e. ZZ ) |
20 |
|
dvdsmul2 |
|- ( ( ( # ` ( X /. ( G ~QG Y ) ) ) e. ZZ /\ ( # ` Y ) e. ZZ ) -> ( # ` Y ) || ( ( # ` ( X /. ( G ~QG Y ) ) ) x. ( # ` Y ) ) ) |
21 |
12 19 20
|
syl2anc |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` Y ) || ( ( # ` ( X /. ( G ~QG Y ) ) ) x. ( # ` Y ) ) ) |
22 |
|
simpl |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> Y e. ( SubGrp ` G ) ) |
23 |
1 5 22 2
|
lagsubg2 |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` X ) = ( ( # ` ( X /. ( G ~QG Y ) ) ) x. ( # ` Y ) ) ) |
24 |
21 23
|
breqtrrd |
|- ( ( Y e. ( SubGrp ` G ) /\ X e. Fin ) -> ( # ` Y ) || ( # ` X ) ) |