This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem odbezout

Description: If N is coprime to the order of A , there is a modular inverse x to cancel multiplication by N . (Contributed by Mario Carneiro, 27-Apr-2016)

Ref Expression
Hypotheses odmulgid.1 
|- X = ( Base ` G )
odmulgid.2 
|- O = ( od ` G )
odmulgid.3 
|- .x. = ( .g ` G )
Assertion odbezout 
|- ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) -> E. x e. ZZ ( x .x. ( N .x. A ) ) = A )

Proof

Step Hyp Ref Expression
1 odmulgid.1 
 |-  X = ( Base ` G )
2 odmulgid.2 
 |-  O = ( od ` G )
3 odmulgid.3 
 |-  .x. = ( .g ` G )
4 simpl3 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) -> N e. ZZ )
5 simpl2 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) -> A e. X )
6 1 2 odcl 
 |-  ( A e. X -> ( O ` A ) e. NN0 )
7 5 6 syl 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) -> ( O ` A ) e. NN0 )
8 7 nn0zd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) -> ( O ` A ) e. ZZ )
9 bezout 
 |-  ( ( N e. ZZ /\ ( O ` A ) e. ZZ ) -> E. x e. ZZ E. y e. ZZ ( N gcd ( O ` A ) ) = ( ( N x. x ) + ( ( O ` A ) x. y ) ) )
10 4 8 9 syl2anc 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) -> E. x e. ZZ E. y e. ZZ ( N gcd ( O ` A ) ) = ( ( N x. x ) + ( ( O ` A ) x. y ) ) )
11 oveq1 
 |-  ( ( ( N x. x ) + ( ( O ` A ) x. y ) ) = ( N gcd ( O ` A ) ) -> ( ( ( N x. x ) + ( ( O ` A ) x. y ) ) .x. A ) = ( ( N gcd ( O ` A ) ) .x. A ) )
12 11 eqcoms 
 |-  ( ( N gcd ( O ` A ) ) = ( ( N x. x ) + ( ( O ` A ) x. y ) ) -> ( ( ( N x. x ) + ( ( O ` A ) x. y ) ) .x. A ) = ( ( N gcd ( O ` A ) ) .x. A ) )
13 simpll1 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> G e. Grp )
14 4 adantr 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> N e. ZZ )
15 simprl 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> x e. ZZ )
16 14 15 zmulcld 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( N x. x ) e. ZZ )
17 5 adantr 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> A e. X )
18 17 6 syl 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( O ` A ) e. NN0 )
19 18 nn0zd 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( O ` A ) e. ZZ )
20 simprr 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> y e. ZZ )
21 19 20 zmulcld 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( O ` A ) x. y ) e. ZZ )
22 eqid 
 |-  ( +g ` G ) = ( +g ` G )
23 1 3 22 mulgdir 
 |-  ( ( G e. Grp /\ ( ( N x. x ) e. ZZ /\ ( ( O ` A ) x. y ) e. ZZ /\ A e. X ) ) -> ( ( ( N x. x ) + ( ( O ` A ) x. y ) ) .x. A ) = ( ( ( N x. x ) .x. A ) ( +g ` G ) ( ( ( O ` A ) x. y ) .x. A ) ) )
24 13 16 21 17 23 syl13anc 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( N x. x ) + ( ( O ` A ) x. y ) ) .x. A ) = ( ( ( N x. x ) .x. A ) ( +g ` G ) ( ( ( O ` A ) x. y ) .x. A ) ) )
25 14 zcnd 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> N e. CC )
26 15 zcnd 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> x e. CC )
27 25 26 mulcomd 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( N x. x ) = ( x x. N ) )
28 27 oveq1d 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( N x. x ) .x. A ) = ( ( x x. N ) .x. A ) )
29 1 3 mulgass 
 |-  ( ( G e. Grp /\ ( x e. ZZ /\ N e. ZZ /\ A e. X ) ) -> ( ( x x. N ) .x. A ) = ( x .x. ( N .x. A ) ) )
30 13 15 14 17 29 syl13anc 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x x. N ) .x. A ) = ( x .x. ( N .x. A ) ) )
31 28 30 eqtrd 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( N x. x ) .x. A ) = ( x .x. ( N .x. A ) ) )
32 dvdsmul1 
 |-  ( ( ( O ` A ) e. ZZ /\ y e. ZZ ) -> ( O ` A ) || ( ( O ` A ) x. y ) )
33 19 20 32 syl2anc 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( O ` A ) || ( ( O ` A ) x. y ) )
34 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
35 1 2 3 34 oddvds 
 |-  ( ( G e. Grp /\ A e. X /\ ( ( O ` A ) x. y ) e. ZZ ) -> ( ( O ` A ) || ( ( O ` A ) x. y ) <-> ( ( ( O ` A ) x. y ) .x. A ) = ( 0g ` G ) ) )
36 13 17 21 35 syl3anc 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( O ` A ) || ( ( O ` A ) x. y ) <-> ( ( ( O ` A ) x. y ) .x. A ) = ( 0g ` G ) ) )
37 33 36 mpbid 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( O ` A ) x. y ) .x. A ) = ( 0g ` G ) )
38 31 37 oveq12d 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( N x. x ) .x. A ) ( +g ` G ) ( ( ( O ` A ) x. y ) .x. A ) ) = ( ( x .x. ( N .x. A ) ) ( +g ` G ) ( 0g ` G ) ) )
39 1 3 mulgcl 
 |-  ( ( G e. Grp /\ N e. ZZ /\ A e. X ) -> ( N .x. A ) e. X )
40 13 14 17 39 syl3anc 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( N .x. A ) e. X )
41 1 3 mulgcl 
 |-  ( ( G e. Grp /\ x e. ZZ /\ ( N .x. A ) e. X ) -> ( x .x. ( N .x. A ) ) e. X )
42 13 15 40 41 syl3anc 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x .x. ( N .x. A ) ) e. X )
43 1 22 34 grprid 
 |-  ( ( G e. Grp /\ ( x .x. ( N .x. A ) ) e. X ) -> ( ( x .x. ( N .x. A ) ) ( +g ` G ) ( 0g ` G ) ) = ( x .x. ( N .x. A ) ) )
44 13 42 43 syl2anc 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( x .x. ( N .x. A ) ) ( +g ` G ) ( 0g ` G ) ) = ( x .x. ( N .x. A ) ) )
45 38 44 eqtrd 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( N x. x ) .x. A ) ( +g ` G ) ( ( ( O ` A ) x. y ) .x. A ) ) = ( x .x. ( N .x. A ) ) )
46 24 45 eqtrd 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( N x. x ) + ( ( O ` A ) x. y ) ) .x. A ) = ( x .x. ( N .x. A ) ) )
47 simplr 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( N gcd ( O ` A ) ) = 1 )
48 47 oveq1d 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( N gcd ( O ` A ) ) .x. A ) = ( 1 .x. A ) )
49 1 3 mulg1 
 |-  ( A e. X -> ( 1 .x. A ) = A )
50 17 49 syl 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( 1 .x. A ) = A )
51 48 50 eqtrd 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( N gcd ( O ` A ) ) .x. A ) = A )
52 46 51 eqeq12d 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( ( N x. x ) + ( ( O ` A ) x. y ) ) .x. A ) = ( ( N gcd ( O ` A ) ) .x. A ) <-> ( x .x. ( N .x. A ) ) = A ) )
53 12 52 imbitrid 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( N gcd ( O ` A ) ) = ( ( N x. x ) + ( ( O ` A ) x. y ) ) -> ( x .x. ( N .x. A ) ) = A ) )
54 53 anassrs 
 |-  ( ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ x e. ZZ ) /\ y e. ZZ ) -> ( ( N gcd ( O ` A ) ) = ( ( N x. x ) + ( ( O ` A ) x. y ) ) -> ( x .x. ( N .x. A ) ) = A ) )
55 54 rexlimdva 
 |-  ( ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) /\ x e. ZZ ) -> ( E. y e. ZZ ( N gcd ( O ` A ) ) = ( ( N x. x ) + ( ( O ` A ) x. y ) ) -> ( x .x. ( N .x. A ) ) = A ) )
56 55 reximdva 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) -> ( E. x e. ZZ E. y e. ZZ ( N gcd ( O ` A ) ) = ( ( N x. x ) + ( ( O ` A ) x. y ) ) -> E. x e. ZZ ( x .x. ( N .x. A ) ) = A ) )
57 10 56 mpd 
 |-  ( ( ( G e. Grp /\ A e. X /\ N e. ZZ ) /\ ( N gcd ( O ` A ) ) = 1 ) -> E. x e. ZZ ( x .x. ( N .x. A ) ) = A )