idomsubgmo

Description: The units of an integral domain have at most one subgroup of any single finite cardinality. (Contributed by Stefan O'Rear, 12-Sep-2015) (Revised by NM, 17-Jun-2017)

		Ref	Expression
	Hypothesis	idomsubgmo.g	$⊢ G = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
	Assertion	idomsubgmo	$⊢ (R \in IDomn \land N \in ℕ) \to \exists^{*} y \in SubGrp (G) \|y\| = N$

Proof

Step	Hyp	Ref	Expression
1		idomsubgmo.g	$⊢ G = {mulGrp}_{R} ↾_{𝑠} Unit (R)$
2		fvex	$⊢ {Base}_{G} \in V$
3	2	rabex	$⊢ \{z \in {Base}_{G} \| od (G) (z) ∥ N\} \in V$
4		simp2l	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to y \in SubGrp (G)$
5		eqid	$⊢ {Base}_{G} = {Base}_{G}$
6	5	subgss	$⊢ y \in SubGrp (G) \to y \subseteq {Base}_{G}$
7	4 6	syl	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to y \subseteq {Base}_{G}$
8		simpl2l	$⊢ (((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \land z \in y) \to y \in SubGrp (G)$
9		simp3l	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to \|y\| = N$
10		simp1r	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to N \in ℕ$
11	10	nnnn0d	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to N \in ℕ_{0}$
12	9 11	eqeltrd	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to \|y\| \in ℕ_{0}$
13		vex	$⊢ y \in V$
14		hashclb	$⊢ y \in V \to (y \in Fin \leftrightarrow \|y\| \in ℕ_{0})$
15	13 14	ax-mp	$⊢ y \in Fin \leftrightarrow \|y\| \in ℕ_{0}$
16	12 15	sylibr	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to y \in Fin$
17	16	adantr	$⊢ (((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \land z \in y) \to y \in Fin$
18		simpr	$⊢ (((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \land z \in y) \to z \in y$
19		eqid	$⊢ od (G) = od (G)$
20	19	odsubdvds	$⊢ (y \in SubGrp (G) \land y \in Fin \land z \in y) \to od (G) (z) ∥ \|y\|$
21	8 17 18 20	syl3anc	$⊢ (((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \land z \in y) \to od (G) (z) ∥ \|y\|$
22	9	adantr	$⊢ (((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \land z \in y) \to \|y\| = N$
23	21 22	breqtrd	$⊢ (((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \land z \in y) \to od (G) (z) ∥ N$
24	7 23	ssrabdv	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to y \subseteq \{z \in {Base}_{G} \| od (G) (z) ∥ N\}$
25		simp2r	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to x \in SubGrp (G)$
26	5	subgss	$⊢ x \in SubGrp (G) \to x \subseteq {Base}_{G}$
27	25 26	syl	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to x \subseteq {Base}_{G}$
28		simpl2r	$⊢ (((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \land z \in x) \to x \in SubGrp (G)$
29		simp3r	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to \|x\| = N$
30	29 11	eqeltrd	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to \|x\| \in ℕ_{0}$
31		vex	$⊢ x \in V$
32		hashclb	$⊢ x \in V \to (x \in Fin \leftrightarrow \|x\| \in ℕ_{0})$
33	31 32	ax-mp	$⊢ x \in Fin \leftrightarrow \|x\| \in ℕ_{0}$
34	30 33	sylibr	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to x \in Fin$
35	34	adantr	$⊢ (((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \land z \in x) \to x \in Fin$
36		simpr	$⊢ (((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \land z \in x) \to z \in x$
37	19	odsubdvds	$⊢ (x \in SubGrp (G) \land x \in Fin \land z \in x) \to od (G) (z) ∥ \|x\|$
38	28 35 36 37	syl3anc	$⊢ (((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \land z \in x) \to od (G) (z) ∥ \|x\|$
39	29	adantr	$⊢ (((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \land z \in x) \to \|x\| = N$
40	38 39	breqtrd	$⊢ (((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \land z \in x) \to od (G) (z) ∥ N$
41	27 40	ssrabdv	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to x \subseteq \{z \in {Base}_{G} \| od (G) (z) ∥ N\}$
42	24 41	unssd	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to y \cup x \subseteq \{z \in {Base}_{G} \| od (G) (z) ∥ N\}$
43		ssdomg	$⊢ \{z \in {Base}_{G} \| od (G) (z) ∥ N\} \in V \to (y \cup x \subseteq \{z \in {Base}_{G} \| od (G) (z) ∥ N\} \to (y \cup x) ≼ \{z \in {Base}_{G} \| od (G) (z) ∥ N\})$
44	3 42 43	mpsyl	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to (y \cup x) ≼ \{z \in {Base}_{G} \| od (G) (z) ∥ N\}$
45	1 5 19	idomodle	$⊢ (R \in IDomn \land N \in ℕ) \to \|\{z \in {Base}_{G} \| od (G) (z) ∥ N\}\| \leq N$
46	45	3ad2ant1	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to \|\{z \in {Base}_{G} \| od (G) (z) ∥ N\}\| \leq N$
47	46 9	breqtrrd	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to \|\{z \in {Base}_{G} \| od (G) (z) ∥ N\}\| \leq \|y\|$
48	3	a1i	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to \{z \in {Base}_{G} \| od (G) (z) ∥ N\} \in V$
49		hashbnd	$⊢ (\{z \in {Base}_{G} \| od (G) (z) ∥ N\} \in V \land \|y\| \in ℕ_{0} \land \|\{z \in {Base}_{G} \| od (G) (z) ∥ N\}\| \leq \|y\|) \to \{z \in {Base}_{G} \| od (G) (z) ∥ N\} \in Fin$
50	48 12 47 49	syl3anc	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to \{z \in {Base}_{G} \| od (G) (z) ∥ N\} \in Fin$
51		hashdom	$⊢ (\{z \in {Base}_{G} \| od (G) (z) ∥ N\} \in Fin \land y \in V) \to (\|\{z \in {Base}_{G} \| od (G) (z) ∥ N\}\| \leq \|y\| \leftrightarrow \{z \in {Base}_{G} \| od (G) (z) ∥ N\} ≼ y)$
52	50 13 51	sylancl	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to (\|\{z \in {Base}_{G} \| od (G) (z) ∥ N\}\| \leq \|y\| \leftrightarrow \{z \in {Base}_{G} \| od (G) (z) ∥ N\} ≼ y)$
53	47 52	mpbid	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to \{z \in {Base}_{G} \| od (G) (z) ∥ N\} ≼ y$
54		domtr	$⊢ ((y \cup x) ≼ \{z \in {Base}_{G} \| od (G) (z) ∥ N\} \land \{z \in {Base}_{G} \| od (G) (z) ∥ N\} ≼ y) \to (y \cup x) ≼ y$
55	44 53 54	syl2anc	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to (y \cup x) ≼ y$
56	13 31	unex	$⊢ y \cup x \in V$
57		ssun1	$⊢ y \subseteq y \cup x$
58		ssdomg	$⊢ y \cup x \in V \to (y \subseteq y \cup x \to y ≼ (y \cup x))$
59	56 57 58	mp2	$⊢ y ≼ (y \cup x)$
60		sbth	$⊢ ((y \cup x) ≼ y \land y ≼ (y \cup x)) \to (y \cup x) \approx y$
61	55 59 60	sylancl	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to (y \cup x) \approx y$
62	9 29	eqtr4d	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to \|y\| = \|x\|$
63		hashen	$⊢ (y \in Fin \land x \in Fin) \to (\|y\| = \|x\| \leftrightarrow y \approx x)$
64	16 34 63	syl2anc	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to (\|y\| = \|x\| \leftrightarrow y \approx x)$
65	62 64	mpbid	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to y \approx x$
66		fiuneneq	$⊢ (y \approx x \land y \in Fin) \to ((y \cup x) \approx y \leftrightarrow y = x)$
67	65 16 66	syl2anc	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to ((y \cup x) \approx y \leftrightarrow y = x)$
68	61 67	mpbid	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G)) \land (\|y\| = N \land \|x\| = N)) \to y = x$
69	68	3expia	$⊢ ((R \in IDomn \land N \in ℕ) \land (y \in SubGrp (G) \land x \in SubGrp (G))) \to ((\|y\| = N \land \|x\| = N) \to y = x)$
70	69	ralrimivva	$⊢ (R \in IDomn \land N \in ℕ) \to \forall y \in SubGrp (G) \forall x \in SubGrp (G) ((\|y\| = N \land \|x\| = N) \to y = x)$
71		fveqeq2	$⊢ y = x \to (\|y\| = N \leftrightarrow \|x\| = N)$
72	71	rmo4	$⊢ \exists^{*} y \in SubGrp (G) \|y\| = N \leftrightarrow \forall y \in SubGrp (G) \forall x \in SubGrp (G) ((\|y\| = N \land \|x\| = N) \to y = x)$
73	70 72	sylibr	$⊢ (R \in IDomn \land N \in ℕ) \to \exists^{*} y \in SubGrp (G) \|y\| = N$

Metamath Proof Explorer

Theorem idomsubgmo

Proof