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	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
Assertion	odbezout	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \to \exists x \in ℤ x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) = A$

Proof

Step	Hyp	Ref	Expression
1		odmulgid.1	$⊢ X = {Base}_{G}$
2		odmulgid.2	$⊢ O = od (G)$
3		odmulgid.3	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
4		simpl3	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \to N \in ℤ$
5		simpl2	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \to A \in X$
6	1 2	odcl	$⊢ A \in X \to O (A) \in ℕ_{0}$
7	5 6	syl	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \to O (A) \in ℕ_{0}$
8	7	nn0zd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \to O (A) \in ℤ$
9		bezout	$⊢ (N \in ℤ \land O (A) \in ℤ) \to \exists x \in ℤ \exists y \in ℤ N \gcd O (A) = N x + O (A) y$
10	4 8 9	syl2anc	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \to \exists x \in ℤ \exists y \in ℤ N \gcd O (A) = N x + O (A) y$
11		oveq1	$⊢ N x + O (A) y = N \gcd O (A) \to (N x + O (A) y) \underset{˙}{\cdot} A = (N \gcd O (A)) \underset{˙}{\cdot} A$
12	11	eqcoms	$⊢ N \gcd O (A) = N x + O (A) y \to (N x + O (A) y) \underset{˙}{\cdot} A = (N \gcd O (A)) \underset{˙}{\cdot} A$
13		simpll1	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to G \in Grp$
14	4	adantr	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to N \in ℤ$
15		simprl	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to x \in ℤ$
16	14 15	zmulcld	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to N x \in ℤ$
17	5	adantr	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to A \in X$
18	17 6	syl	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to O (A) \in ℕ_{0}$
19	18	nn0zd	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to O (A) \in ℤ$
20		simprr	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to y \in ℤ$
21	19 20	zmulcld	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to O (A) y \in ℤ$
22		eqid	$⊢ +_{G} = +_{G}$
23	1 3 22	mulgdir	$⊢ (G \in Grp \land (N x \in ℤ \land O (A) y \in ℤ \land A \in X)) \to (N x + O (A) y) \underset{˙}{\cdot} A = (N x \underset{˙}{\cdot} A) +_{G} (O (A) y \underset{˙}{\cdot} A)$
24	13 16 21 17 23	syl13anc	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to (N x + O (A) y) \underset{˙}{\cdot} A = (N x \underset{˙}{\cdot} A) +_{G} (O (A) y \underset{˙}{\cdot} A)$
25	14	zcnd	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to N \in ℂ$
26	15	zcnd	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to x \in ℂ$
27	25 26	mulcomd	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to N x = x \cdot N$
28	27	oveq1d	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to N x \underset{˙}{\cdot} A = x \cdot N \underset{˙}{\cdot} A$
29	1 3	mulgass	$⊢ (G \in Grp \land (x \in ℤ \land N \in ℤ \land A \in X)) \to x \cdot N \underset{˙}{\cdot} A = x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A)$
30	13 15 14 17 29	syl13anc	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to x \cdot N \underset{˙}{\cdot} A = x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A)$
31	28 30	eqtrd	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to N x \underset{˙}{\cdot} A = x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A)$
32		dvdsmul1	$⊢ (O (A) \in ℤ \land y \in ℤ) \to O (A) ∥ O (A) y$
33	19 20 32	syl2anc	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to O (A) ∥ O (A) y$
34		eqid	$⊢ 0_{G} = 0_{G}$
35	1 2 3 34	oddvds	$⊢ (G \in Grp \land A \in X \land O (A) y \in ℤ) \to (O (A) ∥ O (A) y \leftrightarrow O (A) y \underset{˙}{\cdot} A = 0_{G})$
36	13 17 21 35	syl3anc	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to (O (A) ∥ O (A) y \leftrightarrow O (A) y \underset{˙}{\cdot} A = 0_{G})$
37	33 36	mpbid	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to O (A) y \underset{˙}{\cdot} A = 0_{G}$
38	31 37	oveq12d	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to (N x \underset{˙}{\cdot} A) +_{G} (O (A) y \underset{˙}{\cdot} A) = (x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A)) +_{G} 0_{G}$
39	1 3	mulgcl	$⊢ (G \in Grp \land N \in ℤ \land A \in X) \to N \underset{˙}{\cdot} A \in X$
40	13 14 17 39	syl3anc	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to N \underset{˙}{\cdot} A \in X$
41	1 3	mulgcl	$⊢ (G \in Grp \land x \in ℤ \land N \underset{˙}{\cdot} A \in X) \to x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) \in X$
42	13 15 40 41	syl3anc	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) \in X$
43	1 22 34	grprid	$⊢ (G \in Grp \land x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) \in X) \to (x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A)) +_{G} 0_{G} = x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A)$
44	13 42 43	syl2anc	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to (x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A)) +_{G} 0_{G} = x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A)$
45	38 44	eqtrd	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to (N x \underset{˙}{\cdot} A) +_{G} (O (A) y \underset{˙}{\cdot} A) = x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A)$
46	24 45	eqtrd	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to (N x + O (A) y) \underset{˙}{\cdot} A = x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A)$
47		simplr	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to N \gcd O (A) = 1$
48	47	oveq1d	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to (N \gcd O (A)) \underset{˙}{\cdot} A = 1 \underset{˙}{\cdot} A$
49	1 3	mulg1	$⊢ A \in X \to 1 \underset{˙}{\cdot} A = A$
50	17 49	syl	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to 1 \underset{˙}{\cdot} A = A$
51	48 50	eqtrd	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to (N \gcd O (A)) \underset{˙}{\cdot} A = A$
52	46 51	eqeq12d	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to ((N x + O (A) y) \underset{˙}{\cdot} A = (N \gcd O (A)) \underset{˙}{\cdot} A \leftrightarrow x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) = A)$
53	12 52	syl5ib	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land (x \in ℤ \land y \in ℤ)) \to (N \gcd O (A) = N x + O (A) y \to x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) = A)$
54	53	anassrs	$⊢ ((((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land x \in ℤ) \land y \in ℤ) \to (N \gcd O (A) = N x + O (A) y \to x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) = A)$
55	54	rexlimdva	$⊢ (((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \land x \in ℤ) \to (\exists y \in ℤ N \gcd O (A) = N x + O (A) y \to x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) = A)$
56	55	reximdva	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \to (\exists x \in ℤ \exists y \in ℤ N \gcd O (A) = N x + O (A) y \to \exists x \in ℤ x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) = A)$
57	10 56	mpd	$⊢ ((G \in Grp \land A \in X \land N \in ℤ) \land N \gcd O (A) = 1) \to \exists x \in ℤ x \underset{˙}{\cdot} (N \underset{˙}{\cdot} A) = A$

Metamath Proof Explorer

Theorem odbezout

Proof