Metamath Proof Explorer

Theorem odmodnn0

Description: Reduce the argument of a group multiple by modding out the order of the element. (Contributed by Mario Carneiro, 23-Sep-2015)

Ref Expression
Hypotheses odcl.1 
|- X = ( Base ` G )
odcl.2 
|- O = ( od ` G )
odid.3 
|- .x. = ( .g ` G )
odid.4 
|- .0. = ( 0g ` G )
Assertion odmodnn0 
|- ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( N mod ( O ` A ) ) .x. A ) = ( N .x. A ) )

Proof

Step Hyp Ref Expression
1 odcl.1 
 |-  X = ( Base ` G )
2 odcl.2 
 |-  O = ( od ` G )
3 odid.3 
 |-  .x. = ( .g ` G )
4 odid.4 
 |-  .0. = ( 0g ` G )
5 simpl1 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> G e. Mnd )
6 nnnn0 
 |-  ( ( O ` A ) e. NN -> ( O ` A ) e. NN0 )
7 6 adantl 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. NN0 )
8 simpl3 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> N e. NN0 )
9 8 nn0red 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> N e. RR )
10 nnrp 
 |-  ( ( O ` A ) e. NN -> ( O ` A ) e. RR+ )
11 10 adantl 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. RR+ )
12 9 11 rerpdivcld 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( N / ( O ` A ) ) e. RR )
13 8 nn0ge0d 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> 0 <_ N )
14 nnre 
 |-  ( ( O ` A ) e. NN -> ( O ` A ) e. RR )
15 14 adantl 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. RR )
16 nngt0 
 |-  ( ( O ` A ) e. NN -> 0 < ( O ` A ) )
17 16 adantl 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> 0 < ( O ` A ) )
18 divge0 
 |-  ( ( ( N e. RR /\ 0 <_ N ) /\ ( ( O ` A ) e. RR /\ 0 < ( O ` A ) ) ) -> 0 <_ ( N / ( O ` A ) ) )
19 9 13 15 17 18 syl22anc 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> 0 <_ ( N / ( O ` A ) ) )
20 flge0nn0 
 |-  ( ( ( N / ( O ` A ) ) e. RR /\ 0 <_ ( N / ( O ` A ) ) ) -> ( |_ ` ( N / ( O ` A ) ) ) e. NN0 )
21 12 19 20 syl2anc 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( |_ ` ( N / ( O ` A ) ) ) e. NN0 )
22 7 21 nn0mulcld 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) e. NN0 )
23 8 nn0zd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> N e. ZZ )
24 zmodcl 
 |-  ( ( N e. ZZ /\ ( O ` A ) e. NN ) -> ( N mod ( O ` A ) ) e. NN0 )
25 23 24 sylancom 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( N mod ( O ` A ) ) e. NN0 )
26 simpl2 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> A e. X )
27 eqid 
 |-  ( +g ` G ) = ( +g ` G )
28 1 3 27 mulgnn0dir 
 |-  ( ( G e. Mnd /\ ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) e. NN0 /\ ( N mod ( O ` A ) ) e. NN0 /\ A e. X ) ) -> ( ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) + ( N mod ( O ` A ) ) ) .x. A ) = ( ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) .x. A ) ( +g ` G ) ( ( N mod ( O ` A ) ) .x. A ) ) )
29 5 22 25 26 28 syl13anc 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) + ( N mod ( O ` A ) ) ) .x. A ) = ( ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) .x. A ) ( +g ` G ) ( ( N mod ( O ` A ) ) .x. A ) ) )
30 15 recnd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( O ` A ) e. CC )
31 21 nn0cnd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( |_ ` ( N / ( O ` A ) ) ) e. CC )
32 30 31 mulcomd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) = ( ( |_ ` ( N / ( O ` A ) ) ) x. ( O ` A ) ) )
33 32 oveq1d 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) .x. A ) = ( ( ( |_ ` ( N / ( O ` A ) ) ) x. ( O ` A ) ) .x. A ) )
34 1 3 mulgnn0ass 
 |-  ( ( G e. Mnd /\ ( ( |_ ` ( N / ( O ` A ) ) ) e. NN0 /\ ( O ` A ) e. NN0 /\ A e. X ) ) -> ( ( ( |_ ` ( N / ( O ` A ) ) ) x. ( O ` A ) ) .x. A ) = ( ( |_ ` ( N / ( O ` A ) ) ) .x. ( ( O ` A ) .x. A ) ) )
35 5 21 7 26 34 syl13anc 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( |_ ` ( N / ( O ` A ) ) ) x. ( O ` A ) ) .x. A ) = ( ( |_ ` ( N / ( O ` A ) ) ) .x. ( ( O ` A ) .x. A ) ) )
36 1 2 3 4 odid 
 |-  ( A e. X -> ( ( O ` A ) .x. A ) = .0. )
37 26 36 syl 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) .x. A ) = .0. )
38 37 oveq2d 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( |_ ` ( N / ( O ` A ) ) ) .x. ( ( O ` A ) .x. A ) ) = ( ( |_ ` ( N / ( O ` A ) ) ) .x. .0. ) )
39 1 3 4 mulgnn0z 
 |-  ( ( G e. Mnd /\ ( |_ ` ( N / ( O ` A ) ) ) e. NN0 ) -> ( ( |_ ` ( N / ( O ` A ) ) ) .x. .0. ) = .0. )
40 5 21 39 syl2anc 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( |_ ` ( N / ( O ` A ) ) ) .x. .0. ) = .0. )
41 38 40 eqtrd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( |_ ` ( N / ( O ` A ) ) ) .x. ( ( O ` A ) .x. A ) ) = .0. )
42 35 41 eqtrd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( |_ ` ( N / ( O ` A ) ) ) x. ( O ` A ) ) .x. A ) = .0. )
43 33 42 eqtrd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) .x. A ) = .0. )
44 43 oveq1d 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) .x. A ) ( +g ` G ) ( ( N mod ( O ` A ) ) .x. A ) ) = ( .0. ( +g ` G ) ( ( N mod ( O ` A ) ) .x. A ) ) )
45 29 44 eqtrd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) + ( N mod ( O ` A ) ) ) .x. A ) = ( .0. ( +g ` G ) ( ( N mod ( O ` A ) ) .x. A ) ) )
46 modval 
 |-  ( ( N e. RR /\ ( O ` A ) e. RR+ ) -> ( N mod ( O ` A ) ) = ( N - ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) ) )
47 9 11 46 syl2anc 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( N mod ( O ` A ) ) = ( N - ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) ) )
48 47 oveq2d 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) + ( N mod ( O ` A ) ) ) = ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) + ( N - ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) ) ) )
49 22 nn0cnd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) e. CC )
50 8 nn0cnd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> N e. CC )
51 49 50 pncan3d 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) + ( N - ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) ) ) = N )
52 48 51 eqtrd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) + ( N mod ( O ` A ) ) ) = N )
53 52 oveq1d 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( ( ( O ` A ) x. ( |_ ` ( N / ( O ` A ) ) ) ) + ( N mod ( O ` A ) ) ) .x. A ) = ( N .x. A ) )
54 1 3 mulgnn0cl 
 |-  ( ( G e. Mnd /\ ( N mod ( O ` A ) ) e. NN0 /\ A e. X ) -> ( ( N mod ( O ` A ) ) .x. A ) e. X )
55 5 25 26 54 syl3anc 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( N mod ( O ` A ) ) .x. A ) e. X )
56 1 27 4 mndlid 
 |-  ( ( G e. Mnd /\ ( ( N mod ( O ` A ) ) .x. A ) e. X ) -> ( .0. ( +g ` G ) ( ( N mod ( O ` A ) ) .x. A ) ) = ( ( N mod ( O ` A ) ) .x. A ) )
57 5 55 56 syl2anc 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( .0. ( +g ` G ) ( ( N mod ( O ` A ) ) .x. A ) ) = ( ( N mod ( O ` A ) ) .x. A ) )
58 45 53 57 3eqtr3rd 
 |-  ( ( ( G e. Mnd /\ A e. X /\ N e. NN0 ) /\ ( O ` A ) e. NN ) -> ( ( N mod ( O ` A ) ) .x. A ) = ( N .x. A ) )