odf1o1

Description: An element with zero order has infinitely many multiples. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypotheses	odf1o1.x	$⊢ X = {Base}_{G}$
	odf1o1.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
	odf1o1.o	$⊢ O = od (G)$
	odf1o1.k	$⊢ K = mrCls (SubGrp (G))$
Assertion	odf1o1	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to (x \in ℤ ⟼ x \underset{˙}{\cdot} A) : ℤ \underset{1-1 onto}{⟶} K (\{A\})$

Proof

Step	Hyp	Ref	Expression
1		odf1o1.x	$⊢ X = {Base}_{G}$
2		odf1o1.t	$⊢ \underset{˙}{\cdot} = \cdot_{G}$
3		odf1o1.o	$⊢ O = od (G)$
4		odf1o1.k	$⊢ K = mrCls (SubGrp (G))$
5		simpl1	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land x \in ℤ) \to G \in Grp$
6	1	subgacs	$⊢ G \in Grp \to SubGrp (G) \in ACS (X)$
7		acsmre	$⊢ SubGrp (G) \in ACS (X) \to SubGrp (G) \in Moore (X)$
8	5 6 7	3syl	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land x \in ℤ) \to SubGrp (G) \in Moore (X)$
9		simpl2	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land x \in ℤ) \to A \in X$
10	9	snssd	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land x \in ℤ) \to \{A\} \subseteq X$
11	4	mrccl	$⊢ (SubGrp (G) \in Moore (X) \land \{A\} \subseteq X) \to K (\{A\}) \in SubGrp (G)$
12	8 10 11	syl2anc	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land x \in ℤ) \to K (\{A\}) \in SubGrp (G)$
13		simpr	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land x \in ℤ) \to x \in ℤ$
14	8 4 10	mrcssidd	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land x \in ℤ) \to \{A\} \subseteq K (\{A\})$
15		snidg	$⊢ A \in X \to A \in \{A\}$
16	9 15	syl	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land x \in ℤ) \to A \in \{A\}$
17	14 16	sseldd	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land x \in ℤ) \to A \in K (\{A\})$
18	2	subgmulgcl	$⊢ (K (\{A\}) \in SubGrp (G) \land x \in ℤ \land A \in K (\{A\})) \to x \underset{˙}{\cdot} A \in K (\{A\})$
19	12 13 17 18	syl3anc	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land x \in ℤ) \to x \underset{˙}{\cdot} A \in K (\{A\})$
20	19	ex	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to (x \in ℤ \to x \underset{˙}{\cdot} A \in K (\{A\}))$
21		simpl3	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land (x \in ℤ \land y \in ℤ)) \to O (A) = 0$
22	21	breq1d	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land (x \in ℤ \land y \in ℤ)) \to (O (A) ∥ (x - y) \leftrightarrow 0 ∥ (x - y))$
23		zsubcl	$⊢ (x \in ℤ \land y \in ℤ) \to x - y \in ℤ$
24	23	adantl	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land (x \in ℤ \land y \in ℤ)) \to x - y \in ℤ$
25		0dvds	$⊢ x - y \in ℤ \to (0 ∥ (x - y) \leftrightarrow x - y = 0)$
26	24 25	syl	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land (x \in ℤ \land y \in ℤ)) \to (0 ∥ (x - y) \leftrightarrow x - y = 0)$
27	22 26	bitrd	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land (x \in ℤ \land y \in ℤ)) \to (O (A) ∥ (x - y) \leftrightarrow x - y = 0)$
28		simpl1	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land (x \in ℤ \land y \in ℤ)) \to G \in Grp$
29		simpl2	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land (x \in ℤ \land y \in ℤ)) \to A \in X$
30		simprl	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land (x \in ℤ \land y \in ℤ)) \to x \in ℤ$
31		simprr	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land (x \in ℤ \land y \in ℤ)) \to y \in ℤ$
32		eqid	$⊢ 0_{G} = 0_{G}$
33	1 3 2 32	odcong	$⊢ (G \in Grp \land A \in X \land (x \in ℤ \land y \in ℤ)) \to (O (A) ∥ (x - y) \leftrightarrow x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A)$
34	28 29 30 31 33	syl112anc	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land (x \in ℤ \land y \in ℤ)) \to (O (A) ∥ (x - y) \leftrightarrow x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A)$
35		zcn	$⊢ x \in ℤ \to x \in ℂ$
36		zcn	$⊢ y \in ℤ \to y \in ℂ$
37		subeq0	$⊢ (x \in ℂ \land y \in ℂ) \to (x - y = 0 \leftrightarrow x = y)$
38	35 36 37	syl2an	$⊢ (x \in ℤ \land y \in ℤ) \to (x - y = 0 \leftrightarrow x = y)$
39	38	adantl	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land (x \in ℤ \land y \in ℤ)) \to (x - y = 0 \leftrightarrow x = y)$
40	27 34 39	3bitr3d	$⊢ ((G \in Grp \land A \in X \land O (A) = 0) \land (x \in ℤ \land y \in ℤ)) \to (x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A \leftrightarrow x = y)$
41	40	ex	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to ((x \in ℤ \land y \in ℤ) \to (x \underset{˙}{\cdot} A = y \underset{˙}{\cdot} A \leftrightarrow x = y))$
42	20 41	dom2lem	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to (x \in ℤ ⟼ x \underset{˙}{\cdot} A) : ℤ \underset{1-1}{⟶} K (\{A\})$
43	19	fmpttd	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to (x \in ℤ ⟼ x \underset{˙}{\cdot} A) : ℤ ⟶ K (\{A\})$
44		eqid	$⊢ (x \in ℤ ⟼ x \underset{˙}{\cdot} A) = (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
45	1 2 44 4	cycsubg2	$⊢ (G \in Grp \land A \in X) \to K (\{A\}) = ran (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
46	45	3adant3	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to K (\{A\}) = ran (x \in ℤ ⟼ x \underset{˙}{\cdot} A)$
47	46	eqcomd	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to ran (x \in ℤ ⟼ x \underset{˙}{\cdot} A) = K (\{A\})$
48		dffo2	$⊢ (x \in ℤ ⟼ x \underset{˙}{\cdot} A) : ℤ \underset{onto}{⟶} K (\{A\}) \leftrightarrow ((x \in ℤ ⟼ x \underset{˙}{\cdot} A) : ℤ ⟶ K (\{A\}) \land ran (x \in ℤ ⟼ x \underset{˙}{\cdot} A) = K (\{A\}))$
49	43 47 48	sylanbrc	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to (x \in ℤ ⟼ x \underset{˙}{\cdot} A) : ℤ \underset{onto}{⟶} K (\{A\})$
50		df-f1o	$⊢ (x \in ℤ ⟼ x \underset{˙}{\cdot} A) : ℤ \underset{1-1 onto}{⟶} K (\{A\}) \leftrightarrow ((x \in ℤ ⟼ x \underset{˙}{\cdot} A) : ℤ \underset{1-1}{⟶} K (\{A\}) \land (x \in ℤ ⟼ x \underset{˙}{\cdot} A) : ℤ \underset{onto}{⟶} K (\{A\}))$
51	42 49 50	sylanbrc	$⊢ (G \in Grp \land A \in X \land O (A) = 0) \to (x \in ℤ ⟼ x \underset{˙}{\cdot} A) : ℤ \underset{1-1 onto}{⟶} K (\{A\})$

Metamath Proof Explorer

Theorem odf1o1

Proof