Step |
Hyp |
Ref |
Expression |
1 |
|
cycsubmcom.b |
|- B = ( Base ` G ) |
2 |
|
cycsubmcom.t |
|- .x. = ( .g ` G ) |
3 |
|
cycsubmcom.f |
|- F = ( x e. NN0 |-> ( x .x. A ) ) |
4 |
|
cycsubmcom.c |
|- C = ran F |
5 |
|
cycsubmcom.p |
|- .+ = ( +g ` G ) |
6 |
1 2 3 4
|
cycsubmel |
|- ( c e. C <-> E. i e. NN0 c = ( i .x. A ) ) |
7 |
6
|
biimpi |
|- ( c e. C -> E. i e. NN0 c = ( i .x. A ) ) |
8 |
7
|
adantl |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ c e. C ) -> E. i e. NN0 c = ( i .x. A ) ) |
9 |
8
|
ralrimiva |
|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> A. c e. C E. i e. NN0 c = ( i .x. A ) ) |
10 |
|
simplll |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> G e. Mnd ) |
11 |
|
simprl |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> m e. NN0 ) |
12 |
|
simprr |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> n e. NN0 ) |
13 |
|
simpllr |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> A e. B ) |
14 |
1 2 5
|
mulgnn0dir |
|- ( ( G e. Mnd /\ ( m e. NN0 /\ n e. NN0 /\ A e. B ) ) -> ( ( m + n ) .x. A ) = ( ( m .x. A ) .+ ( n .x. A ) ) ) |
15 |
10 11 12 13 14
|
syl13anc |
|- ( ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) /\ ( m e. NN0 /\ n e. NN0 ) ) -> ( ( m + n ) .x. A ) = ( ( m .x. A ) .+ ( n .x. A ) ) ) |
16 |
15
|
ralrimivva |
|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> A. m e. NN0 A. n e. NN0 ( ( m + n ) .x. A ) = ( ( m .x. A ) .+ ( n .x. A ) ) ) |
17 |
|
simprl |
|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> X e. C ) |
18 |
|
simprr |
|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> Y e. C ) |
19 |
|
nn0sscn |
|- NN0 C_ CC |
20 |
19
|
a1i |
|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> NN0 C_ CC ) |
21 |
9 16 17 18 20
|
cyccom |
|- ( ( ( G e. Mnd /\ A e. B ) /\ ( X e. C /\ Y e. C ) ) -> ( X .+ Y ) = ( Y .+ X ) ) |