Step |
Hyp |
Ref |
Expression |
1 |
|
cycsubm.b |
|- B = ( Base ` G ) |
2 |
|
cycsubm.t |
|- .x. = ( .g ` G ) |
3 |
|
cycsubm.f |
|- F = ( x e. NN0 |-> ( x .x. A ) ) |
4 |
|
cycsubm.c |
|- C = ran F |
5 |
1 2
|
mulgnn0cl |
|- ( ( G e. Mnd /\ x e. NN0 /\ A e. B ) -> ( x .x. A ) e. B ) |
6 |
5
|
3expa |
|- ( ( ( G e. Mnd /\ x e. NN0 ) /\ A e. B ) -> ( x .x. A ) e. B ) |
7 |
6
|
an32s |
|- ( ( ( G e. Mnd /\ A e. B ) /\ x e. NN0 ) -> ( x .x. A ) e. B ) |
8 |
7 3
|
fmptd |
|- ( ( G e. Mnd /\ A e. B ) -> F : NN0 --> B ) |
9 |
8
|
frnd |
|- ( ( G e. Mnd /\ A e. B ) -> ran F C_ B ) |
10 |
4 9
|
eqsstrid |
|- ( ( G e. Mnd /\ A e. B ) -> C C_ B ) |
11 |
|
0nn0 |
|- 0 e. NN0 |
12 |
11
|
a1i |
|- ( ( G e. Mnd /\ A e. B ) -> 0 e. NN0 ) |
13 |
|
oveq1 |
|- ( i = 0 -> ( i .x. A ) = ( 0 .x. A ) ) |
14 |
13
|
eqeq2d |
|- ( i = 0 -> ( ( 0g ` G ) = ( i .x. A ) <-> ( 0g ` G ) = ( 0 .x. A ) ) ) |
15 |
14
|
adantl |
|- ( ( ( G e. Mnd /\ A e. B ) /\ i = 0 ) -> ( ( 0g ` G ) = ( i .x. A ) <-> ( 0g ` G ) = ( 0 .x. A ) ) ) |
16 |
|
eqid |
|- ( 0g ` G ) = ( 0g ` G ) |
17 |
1 16 2
|
mulg0 |
|- ( A e. B -> ( 0 .x. A ) = ( 0g ` G ) ) |
18 |
17
|
adantl |
|- ( ( G e. Mnd /\ A e. B ) -> ( 0 .x. A ) = ( 0g ` G ) ) |
19 |
18
|
eqcomd |
|- ( ( G e. Mnd /\ A e. B ) -> ( 0g ` G ) = ( 0 .x. A ) ) |
20 |
12 15 19
|
rspcedvd |
|- ( ( G e. Mnd /\ A e. B ) -> E. i e. NN0 ( 0g ` G ) = ( i .x. A ) ) |
21 |
1 2 3 4
|
cycsubmel |
|- ( ( 0g ` G ) e. C <-> E. i e. NN0 ( 0g ` G ) = ( i .x. A ) ) |
22 |
20 21
|
sylibr |
|- ( ( G e. Mnd /\ A e. B ) -> ( 0g ` G ) e. C ) |
23 |
|
simplr |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> i e. NN0 ) |
24 |
|
simpr |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> j e. NN0 ) |
25 |
23 24
|
nn0addcld |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> ( i + j ) e. NN0 ) |
26 |
25
|
adantr |
|- ( ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) /\ ( b = ( j .x. A ) /\ a = ( i .x. A ) ) ) -> ( i + j ) e. NN0 ) |
27 |
|
oveq1 |
|- ( k = ( i + j ) -> ( k .x. A ) = ( ( i + j ) .x. A ) ) |
28 |
27
|
eqeq2d |
|- ( k = ( i + j ) -> ( ( a ( +g ` G ) b ) = ( k .x. A ) <-> ( a ( +g ` G ) b ) = ( ( i + j ) .x. A ) ) ) |
29 |
28
|
adantl |
|- ( ( ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) /\ ( b = ( j .x. A ) /\ a = ( i .x. A ) ) ) /\ k = ( i + j ) ) -> ( ( a ( +g ` G ) b ) = ( k .x. A ) <-> ( a ( +g ` G ) b ) = ( ( i + j ) .x. A ) ) ) |
30 |
|
oveq12 |
|- ( ( a = ( i .x. A ) /\ b = ( j .x. A ) ) -> ( a ( +g ` G ) b ) = ( ( i .x. A ) ( +g ` G ) ( j .x. A ) ) ) |
31 |
30
|
ancoms |
|- ( ( b = ( j .x. A ) /\ a = ( i .x. A ) ) -> ( a ( +g ` G ) b ) = ( ( i .x. A ) ( +g ` G ) ( j .x. A ) ) ) |
32 |
|
simplll |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> G e. Mnd ) |
33 |
|
simpllr |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> A e. B ) |
34 |
|
eqid |
|- ( +g ` G ) = ( +g ` G ) |
35 |
1 2 34
|
mulgnn0dir |
|- ( ( G e. Mnd /\ ( i e. NN0 /\ j e. NN0 /\ A e. B ) ) -> ( ( i + j ) .x. A ) = ( ( i .x. A ) ( +g ` G ) ( j .x. A ) ) ) |
36 |
32 23 24 33 35
|
syl13anc |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> ( ( i + j ) .x. A ) = ( ( i .x. A ) ( +g ` G ) ( j .x. A ) ) ) |
37 |
36
|
eqcomd |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> ( ( i .x. A ) ( +g ` G ) ( j .x. A ) ) = ( ( i + j ) .x. A ) ) |
38 |
31 37
|
sylan9eqr |
|- ( ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) /\ ( b = ( j .x. A ) /\ a = ( i .x. A ) ) ) -> ( a ( +g ` G ) b ) = ( ( i + j ) .x. A ) ) |
39 |
26 29 38
|
rspcedvd |
|- ( ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) /\ ( b = ( j .x. A ) /\ a = ( i .x. A ) ) ) -> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) ) |
40 |
39
|
exp32 |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) /\ j e. NN0 ) -> ( b = ( j .x. A ) -> ( a = ( i .x. A ) -> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) ) ) ) |
41 |
40
|
rexlimdva |
|- ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) -> ( E. j e. NN0 b = ( j .x. A ) -> ( a = ( i .x. A ) -> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) ) ) ) |
42 |
41
|
com23 |
|- ( ( ( G e. Mnd /\ A e. B ) /\ i e. NN0 ) -> ( a = ( i .x. A ) -> ( E. j e. NN0 b = ( j .x. A ) -> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) ) ) ) |
43 |
42
|
rexlimdva |
|- ( ( G e. Mnd /\ A e. B ) -> ( E. i e. NN0 a = ( i .x. A ) -> ( E. j e. NN0 b = ( j .x. A ) -> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) ) ) ) |
44 |
43
|
impd |
|- ( ( G e. Mnd /\ A e. B ) -> ( ( E. i e. NN0 a = ( i .x. A ) /\ E. j e. NN0 b = ( j .x. A ) ) -> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) ) ) |
45 |
1 2 3 4
|
cycsubmel |
|- ( a e. C <-> E. i e. NN0 a = ( i .x. A ) ) |
46 |
1 2 3 4
|
cycsubmel |
|- ( b e. C <-> E. j e. NN0 b = ( j .x. A ) ) |
47 |
45 46
|
anbi12i |
|- ( ( a e. C /\ b e. C ) <-> ( E. i e. NN0 a = ( i .x. A ) /\ E. j e. NN0 b = ( j .x. A ) ) ) |
48 |
1 2 3 4
|
cycsubmel |
|- ( ( a ( +g ` G ) b ) e. C <-> E. k e. NN0 ( a ( +g ` G ) b ) = ( k .x. A ) ) |
49 |
44 47 48
|
3imtr4g |
|- ( ( G e. Mnd /\ A e. B ) -> ( ( a e. C /\ b e. C ) -> ( a ( +g ` G ) b ) e. C ) ) |
50 |
49
|
ralrimivv |
|- ( ( G e. Mnd /\ A e. B ) -> A. a e. C A. b e. C ( a ( +g ` G ) b ) e. C ) |
51 |
1 16 34
|
issubm |
|- ( G e. Mnd -> ( C e. ( SubMnd ` G ) <-> ( C C_ B /\ ( 0g ` G ) e. C /\ A. a e. C A. b e. C ( a ( +g ` G ) b ) e. C ) ) ) |
52 |
51
|
adantr |
|- ( ( G e. Mnd /\ A e. B ) -> ( C e. ( SubMnd ` G ) <-> ( C C_ B /\ ( 0g ` G ) e. C /\ A. a e. C A. b e. C ( a ( +g ` G ) b ) e. C ) ) ) |
53 |
10 22 50 52
|
mpbir3and |
|- ( ( G e. Mnd /\ A e. B ) -> C e. ( SubMnd ` G ) ) |