cyc3evpm - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > cyc3evpm		Structured version Visualization version GIF version

Theorem cyc3evpm 33781

Description: 3-Cycles are even permutations. (Contributed by Thierry Arnoux, 24-Sep-2023.)

**Hypotheses**
Ref	Expression
cyc3evpm.t	⊢ 𝐶 = ((toCyc‘𝐷) “ (^◡♯ “ {3}))
cyc3evpm.a	⊢ 𝐴 = (pmEven‘𝐷)

**Assertion**
Ref	Expression
cyc3evpm	⊢ (𝐷 ∈ Fin → 𝐶 ⊆ 𝐴)

Proof of Theorem cyc3evpm Dummy variables 𝑝 𝑢 𝑤 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 490	. . . . 5 ⊢ ((((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) ∧ ((toCyc‘𝐷)‘𝑢) = 𝑝) → ((toCyc‘𝐷)‘𝑢) = 𝑝)
2		simpl 488	. . . . . . . 8 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → 𝐷 ∈ Fin)
3		eqid 2763	. . . . . . . . 9 ⊢ (toCyc‘𝐷) = (toCyc‘𝐷)
4		simpr 490	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3})))
5	4	elin1d 4104	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → 𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷})
6		elrabi 3644	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} → 𝑢 ∈ Word 𝐷)
7	5, 6	syl 18	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → 𝑢 ∈ Word 𝐷)
8		id 23	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → 𝑤 = 𝑢)
9		dmeq 5892	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → dom 𝑤 = dom 𝑢)
10		eqidd 2764	. . . . . . . . . . . . 13 ⊢ (𝑤 = 𝑢 → 𝐷 = 𝐷)
11	8, 9, 10	f1eq123d 6838	. . . . . . . . . . . 12 ⊢ (𝑤 = 𝑢 → (𝑤:dom 𝑤⟶1-1𝐷 ↔ 𝑢:dom 𝑢⟶1-1𝐷))
12	11	elrab 3648	. . . . . . . . . . 11 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ↔ (𝑢 ∈ Word 𝐷 ∧ 𝑢:dom 𝑢⟶1-1𝐷))
13	12	simprbi 503	. . . . . . . . . 10 ⊢ (𝑢 ∈ {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} → 𝑢:dom 𝑢⟶1-1𝐷)
14	5, 13	syl 18	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → 𝑢:dom 𝑢⟶1-1𝐷)
15		eqid 2763	. . . . . . . . 9 ⊢ (SymGrp‘𝐷) = (SymGrp‘𝐷)
16	3, 2, 7, 14, 15	cycpmcl 33747	. . . . . . . 8 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((toCyc‘𝐷)‘𝑢) ∈ (Base‘(SymGrp‘𝐷)))
17		c0ex 11327	. . . . . . . . . . . . . . . . . 18 ⊢ 0 ∈ V
18	17	tpid1 4729	. . . . . . . . . . . . . . . . 17 ⊢ 0 ∈ {0, 1, 2}
19		fzo0to3tp 13914	. . . . . . . . . . . . . . . . 17 ⊢ (0..^3) = {0, 1, 2}
20	18, 19	eleqtrri 2863	. . . . . . . . . . . . . . . 16 ⊢ 0 ∈ (0..^3)
21	4	elin2d 4105	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → 𝑢 ∈ (^◡♯ “ {3}))
22		hashf 14509	. . . . . . . . . . . . . . . . . . . 20 ⊢ ♯:V⟶(ℕ₀ ∪ {+∞})
23		ffn 6731	. . . . . . . . . . . . . . . . . . . 20 ⊢ (♯:V⟶(ℕ₀ ∪ {+∞}) → ♯ Fn V)
24		elpreima 7080	. . . . . . . . . . . . . . . . . . . 20 ⊢ (♯ Fn V → (𝑢 ∈ (^◡♯ “ {3}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) ∈ {3})))
25	22, 23, 24	mp2b 10	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑢 ∈ (^◡♯ “ {3}) ↔ (𝑢 ∈ V ∧ (♯‘𝑢) ∈ {3}))
26	25	simprbi 503	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ (^◡♯ “ {3}) → (♯‘𝑢) ∈ {3})
27		elsni 4601	. . . . . . . . . . . . . . . . . 18 ⊢ ((♯‘𝑢) ∈ {3} → (♯‘𝑢) = 3)
28	21, 26, 27	3syl 19	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (♯‘𝑢) = 3)
29	28	oveq2d 7459	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (0..^(♯‘𝑢)) = (0..^3))
30	20, 29	eleqtrrid 2871	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → 0 ∈ (0..^(♯‘𝑢)))
31		wrdsymbcl 14699	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ Word 𝐷 ∧ 0 ∈ (0..^(♯‘𝑢))) → (𝑢‘0) ∈ 𝐷)
32	7, 30, 31	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (𝑢‘0) ∈ 𝐷)
33		1eltp012 12440	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ {0, 1, 2}
34	33, 19	eleqtrri 2863	. . . . . . . . . . . . . . . 16 ⊢ 1 ∈ (0..^3)
35	34, 29	eleqtrrid 2871	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → 1 ∈ (0..^(♯‘𝑢)))
36		wrdsymbcl 14699	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ Word 𝐷 ∧ 1 ∈ (0..^(♯‘𝑢))) → (𝑢‘1) ∈ 𝐷)
37	7, 35, 36	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (𝑢‘1) ∈ 𝐷)
38		2ex 12447	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ V
39	38	tpid3 4734	. . . . . . . . . . . . . . . . 17 ⊢ 2 ∈ {0, 1, 2}
40	39, 19	eleqtrri 2863	. . . . . . . . . . . . . . . 16 ⊢ 2 ∈ (0..^3)
41	40, 29	eleqtrrid 2871	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → 2 ∈ (0..^(♯‘𝑢)))
42		wrdsymbcl 14699	. . . . . . . . . . . . . . 15 ⊢ ((𝑢 ∈ Word 𝐷 ∧ 2 ∈ (0..^(♯‘𝑢))) → (𝑢‘2) ∈ 𝐷)
43	7, 41, 42	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (𝑢‘2) ∈ 𝐷)
44	32, 37, 43	3jca 1146	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((𝑢‘0) ∈ 𝐷 ∧ (𝑢‘1) ∈ 𝐷 ∧ (𝑢‘2) ∈ 𝐷))
45		eqidd 2764	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (𝑢‘0) = (𝑢‘0))
46		eqidd 2764	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (𝑢‘1) = (𝑢‘1))
47		eqidd 2764	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (𝑢‘2) = (𝑢‘2))
48	45, 46, 47	3jca 1146	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((𝑢‘0) = (𝑢‘0) ∧ (𝑢‘1) = (𝑢‘1) ∧ (𝑢‘2) = (𝑢‘2)))
49		eqwrds3 15143	. . . . . . . . . . . . . 14 ⊢ ((𝑢 ∈ Word 𝐷 ∧ ((𝑢‘0) ∈ 𝐷 ∧ (𝑢‘1) ∈ 𝐷 ∧ (𝑢‘2) ∈ 𝐷)) → (𝑢 = ⟨“(𝑢‘0)(𝑢‘1)(𝑢‘2)”⟩ ↔ ((♯‘𝑢) = 3 ∧ ((𝑢‘0) = (𝑢‘0) ∧ (𝑢‘1) = (𝑢‘1) ∧ (𝑢‘2) = (𝑢‘2)))))
50	49	biimpar 483	. . . . . . . . . . . . 13 ⊢ (((𝑢 ∈ Word 𝐷 ∧ ((𝑢‘0) ∈ 𝐷 ∧ (𝑢‘1) ∈ 𝐷 ∧ (𝑢‘2) ∈ 𝐷)) ∧ ((♯‘𝑢) = 3 ∧ ((𝑢‘0) = (𝑢‘0) ∧ (𝑢‘1) = (𝑢‘1) ∧ (𝑢‘2) = (𝑢‘2)))) → 𝑢 = ⟨“(𝑢‘0)(𝑢‘1)(𝑢‘2)”⟩)
51	7, 44, 28, 48, 50	syl22anc 852	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → 𝑢 = ⟨“(𝑢‘0)(𝑢‘1)(𝑢‘2)”⟩)
52	51	fveq2d 6912	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((toCyc‘𝐷)‘𝑢) = ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)(𝑢‘2)”⟩))
53		wrddm 14693	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑢 ∈ Word 𝐷 → dom 𝑢 = (0..^(♯‘𝑢)))
54	7, 53	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → dom 𝑢 = (0..^(♯‘𝑢)))
55	54, 29	eqtrd 2798	. . . . . . . . . . . . . . . 16 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → dom 𝑢 = (0..^3))
56	55, 19	eqtrdi 2814	. . . . . . . . . . . . . . 15 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → dom 𝑢 = {0, 1, 2})
57		f1eq2 6796	. . . . . . . . . . . . . . . 16 ⊢ (dom 𝑢 = {0, 1, 2} → (𝑢:dom 𝑢⟶1-1𝐷 ↔ 𝑢:{0, 1, 2}⟶1-1𝐷))
58	57	biimpa 482	. . . . . . . . . . . . . . 15 ⊢ ((dom 𝑢 = {0, 1, 2} ∧ 𝑢:dom 𝑢⟶1-1𝐷) → 𝑢:{0, 1, 2}⟶1-1𝐷)
59	56, 14, 58	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → 𝑢:{0, 1, 2}⟶1-1𝐷)
60		1ex 11330	. . . . . . . . . . . . . . . . 17 ⊢ 1 ∈ V
61	17, 60, 38	3pm3.2i 1358	. . . . . . . . . . . . . . . 16 ⊢ (0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V)
62		0ne1 12441	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 1
63		0ne2 12579	. . . . . . . . . . . . . . . . 17 ⊢ 0 ≠ 2
64		1ne2 12580	. . . . . . . . . . . . . . . . 17 ⊢ 1 ≠ 2
65	62, 63, 64	3pm3.2i 1358	. . . . . . . . . . . . . . . 16 ⊢ (0 ≠ 1 ∧ 0 ≠ 2 ∧ 1 ≠ 2)
66		eqid 2763	. . . . . . . . . . . . . . . . 17 ⊢ {0, 1, 2} = {0, 1, 2}
67	66	f13dfv 7305	. . . . . . . . . . . . . . . 16 ⊢ (((0 ∈ V ∧ 1 ∈ V ∧ 2 ∈ V) ∧ (0 ≠ 1 ∧ 0 ≠ 2 ∧ 1 ≠ 2)) → (𝑢:{0, 1, 2}⟶1-1𝐷 ↔ (𝑢:{0, 1, 2}⟶𝐷 ∧ ((𝑢‘0) ≠ (𝑢‘1) ∧ (𝑢‘0) ≠ (𝑢‘2) ∧ (𝑢‘1) ≠ (𝑢‘2)))))
68	61, 65, 67	mp2an 705	. . . . . . . . . . . . . . 15 ⊢ (𝑢:{0, 1, 2}⟶1-1𝐷 ↔ (𝑢:{0, 1, 2}⟶𝐷 ∧ ((𝑢‘0) ≠ (𝑢‘1) ∧ (𝑢‘0) ≠ (𝑢‘2) ∧ (𝑢‘1) ≠ (𝑢‘2))))
69	68	simprbi 503	. . . . . . . . . . . . . 14 ⊢ (𝑢:{0, 1, 2}⟶1-1𝐷 → ((𝑢‘0) ≠ (𝑢‘1) ∧ (𝑢‘0) ≠ (𝑢‘2) ∧ (𝑢‘1) ≠ (𝑢‘2)))
70	59, 69	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((𝑢‘0) ≠ (𝑢‘1) ∧ (𝑢‘0) ≠ (𝑢‘2) ∧ (𝑢‘1) ≠ (𝑢‘2)))
71	70	simp1d 1160	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (𝑢‘0) ≠ (𝑢‘1))
72	70	simp3d 1162	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (𝑢‘1) ≠ (𝑢‘2))
73	70	simp2d 1161	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (𝑢‘0) ≠ (𝑢‘2))
74	73	necomd 3014	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (𝑢‘2) ≠ (𝑢‘0))
75		eqid 2763	. . . . . . . . . . . 12 ⊢ (+_g‘(SymGrp‘𝐷)) = (+_g‘(SymGrp‘𝐷))
76	3, 15, 2, 32, 37, 43, 71, 72, 74, 75	cyc3co2 33771	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)(𝑢‘2)”⟩) = (((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩)(+_g‘(SymGrp‘𝐷))((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩)))
77	3, 2, 32, 43, 73, 15	cycpm2cl 33751	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩) ∈ (Base‘(SymGrp‘𝐷)))
78	3, 2, 32, 37, 71, 15	cycpm2cl 33751	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩) ∈ (Base‘(SymGrp‘𝐷)))
79		eqid 2763	. . . . . . . . . . . . 13 ⊢ (Base‘(SymGrp‘𝐷)) = (Base‘(SymGrp‘𝐷))
80	15, 79, 75	symgov 19628	. . . . . . . . . . . 12 ⊢ ((((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩) ∈ (Base‘(SymGrp‘𝐷)) ∧ ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩) ∈ (Base‘(SymGrp‘𝐷))) → (((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩)(+_g‘(SymGrp‘𝐷))((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩)) = (((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩) ∘ ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩)))
81	77, 78, 80	syl2anc 596	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩)(+_g‘(SymGrp‘𝐷))((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩)) = (((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩) ∘ ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩)))
82	52, 76, 81	3eqtrd 2802	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((toCyc‘𝐷)‘𝑢) = (((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩) ∘ ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩)))
83	82	fveq2d 6912	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘𝑢)) = ((pmSgn‘𝐷)‘(((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩) ∘ ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩))))
84		eqid 2763	. . . . . . . . . . 11 ⊢ (pmSgn‘𝐷) = (pmSgn‘𝐷)
85	15, 84, 79	psgnco 21919	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩) ∈ (Base‘(SymGrp‘𝐷)) ∧ ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩) ∈ (Base‘(SymGrp‘𝐷))) → ((pmSgn‘𝐷)‘(((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩) ∘ ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩))) = (((pmSgn‘𝐷)‘((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩)) · ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩))))
86	2, 77, 78, 85	syl3anc 1399	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((pmSgn‘𝐷)‘(((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩) ∘ ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩))) = (((pmSgn‘𝐷)‘((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩)) · ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩))))
87		eqid 2763	. . . . . . . . . . . . . 14 ⊢ (pmTrsp‘𝐷) = (pmTrsp‘𝐷)
88	3, 2, 32, 43, 73, 87	cycpm2tr 33750	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩) = ((pmTrsp‘𝐷)‘{(𝑢‘0), (𝑢‘2)}))
89	32, 43	prssd 4781	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → {(𝑢‘0), (𝑢‘2)} ⊆ 𝐷)
90		enpr2 10110	. . . . . . . . . . . . . . 15 ⊢ (((𝑢‘0) ∈ 𝐷 ∧ (𝑢‘2) ∈ 𝐷 ∧ (𝑢‘0) ≠ (𝑢‘2)) → {(𝑢‘0), (𝑢‘2)} ≈ 2_o)
91	32, 43, 73, 90	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → {(𝑢‘0), (𝑢‘2)} ≈ 2_o)
92		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ ran (pmTrsp‘𝐷) = ran (pmTrsp‘𝐷)
93	87, 92	pmtrrn 19701	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ {(𝑢‘0), (𝑢‘2)} ⊆ 𝐷 ∧ {(𝑢‘0), (𝑢‘2)} ≈ 2_o) → ((pmTrsp‘𝐷)‘{(𝑢‘0), (𝑢‘2)}) ∈ ran (pmTrsp‘𝐷))
94	2, 89, 91, 93	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((pmTrsp‘𝐷)‘{(𝑢‘0), (𝑢‘2)}) ∈ ran (pmTrsp‘𝐷))
95	88, 94	eqeltrd 2864	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩) ∈ ran (pmTrsp‘𝐷))
96	15, 92, 84	psgnpmtr 19754	. . . . . . . . . . . 12 ⊢ (((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩) ∈ ran (pmTrsp‘𝐷) → ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩)) = -1)
97	95, 96	syl 18	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩)) = -1)
98	3, 2, 32, 37, 71, 87	cycpm2tr 33750	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩) = ((pmTrsp‘𝐷)‘{(𝑢‘0), (𝑢‘1)}))
99	32, 37	prssd 4781	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → {(𝑢‘0), (𝑢‘1)} ⊆ 𝐷)
100		enpr2 10110	. . . . . . . . . . . . . . 15 ⊢ (((𝑢‘0) ∈ 𝐷 ∧ (𝑢‘1) ∈ 𝐷 ∧ (𝑢‘0) ≠ (𝑢‘1)) → {(𝑢‘0), (𝑢‘1)} ≈ 2_o)
101	32, 37, 71, 100	syl3anc 1399	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → {(𝑢‘0), (𝑢‘1)} ≈ 2_o)
102	87, 92	pmtrrn 19701	. . . . . . . . . . . . . 14 ⊢ ((𝐷 ∈ Fin ∧ {(𝑢‘0), (𝑢‘1)} ⊆ 𝐷 ∧ {(𝑢‘0), (𝑢‘1)} ≈ 2_o) → ((pmTrsp‘𝐷)‘{(𝑢‘0), (𝑢‘1)}) ∈ ran (pmTrsp‘𝐷))
103	2, 99, 101, 102	syl3anc 1399	. . . . . . . . . . . . 13 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((pmTrsp‘𝐷)‘{(𝑢‘0), (𝑢‘1)}) ∈ ran (pmTrsp‘𝐷))
104	98, 103	eqeltrd 2864	. . . . . . . . . . . 12 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩) ∈ ran (pmTrsp‘𝐷))
105	15, 92, 84	psgnpmtr 19754	. . . . . . . . . . . 12 ⊢ (((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩) ∈ ran (pmTrsp‘𝐷) → ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩)) = -1)
106	104, 105	syl 18	. . . . . . . . . . 11 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩)) = -1)
107	97, 106	oveq12d 7461	. . . . . . . . . 10 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (((pmSgn‘𝐷)‘((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩)) · ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩))) = ( -1 · -1))
108		neg1mulneg1e1 12585	. . . . . . . . . 10 ⊢ ( -1 · -1) = 1
109	107, 108	eqtrdi 2814	. . . . . . . . 9 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → (((pmSgn‘𝐷)‘((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘2)”⟩)) · ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘⟨“(𝑢‘0)(𝑢‘1)”⟩))) = 1)
110	83, 86, 109	3eqtrd 2802	. . . . . . . 8 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘𝑢)) = 1)
111	15, 79, 84	psgnevpmb 21923	. . . . . . . . 9 ⊢ (𝐷 ∈ Fin → (((toCyc‘𝐷)‘𝑢) ∈ (pmEven‘𝐷) ↔ (((toCyc‘𝐷)‘𝑢) ∈ (Base‘(SymGrp‘𝐷)) ∧ ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘𝑢)) = 1)))
112	111	biimpar 483	. . . . . . . 8 ⊢ ((𝐷 ∈ Fin ∧ (((toCyc‘𝐷)‘𝑢) ∈ (Base‘(SymGrp‘𝐷)) ∧ ((pmSgn‘𝐷)‘((toCyc‘𝐷)‘𝑢)) = 1)) → ((toCyc‘𝐷)‘𝑢) ∈ (pmEven‘𝐷))
113	2, 16, 110, 112	syl12anc 850	. . . . . . 7 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((toCyc‘𝐷)‘𝑢) ∈ (pmEven‘𝐷))
114		cyc3evpm.a	. . . . . . 7 ⊢ 𝐴 = (pmEven‘𝐷)
115	113, 114	eleqtrrdi 2875	. . . . . 6 ⊢ ((𝐷 ∈ Fin ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) → ((toCyc‘𝐷)‘𝑢) ∈ 𝐴)
116	115	ad4ant13 764	. . . . 5 ⊢ ((((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) ∧ ((toCyc‘𝐷)‘𝑢) = 𝑝) → ((toCyc‘𝐷)‘𝑢) ∈ 𝐴)
117	1, 116	eqeltrrd 2865	. . . 4 ⊢ ((((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) ∧ 𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))) ∧ ((toCyc‘𝐷)‘𝑢) = 𝑝) → 𝑝 ∈ 𝐴)
118		nfcv 2926	. . . . 5 ⊢ Ⅎ𝑢(toCyc‘𝐷)
119	3, 15, 79	tocycf 33748	. . . . . . 7 ⊢ (𝐷 ∈ Fin → (toCyc‘𝐷):{𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷}⟶(Base‘(SymGrp‘𝐷)))
120	119	ffnd 6732	. . . . . 6 ⊢ (𝐷 ∈ Fin → (toCyc‘𝐷) Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷})
121	120	adantr 486	. . . . 5 ⊢ ((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) → (toCyc‘𝐷) Fn {𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷})
122		simpr 490	. . . . . 6 ⊢ ((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) → 𝑝 ∈ 𝐶)
123		cyc3evpm.t	. . . . . 6 ⊢ 𝐶 = ((toCyc‘𝐷) “ (^◡♯ “ {3}))
124	122, 123	eleqtrdi 2874	. . . . 5 ⊢ ((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) → 𝑝 ∈ ((toCyc‘𝐷) “ (^◡♯ “ {3})))
125	118, 121, 124	fvelimad 6975	. . . 4 ⊢ ((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) → ∃𝑢 ∈ ({𝑤 ∈ Word 𝐷 ∣ 𝑤:dom 𝑤⟶1-1𝐷} ∩ (^◡♯ “ {3}))((toCyc‘𝐷)‘𝑢) = 𝑝)
126	117, 125	r19.29a 3174	. . 3 ⊢ ((𝐷 ∈ Fin ∧ 𝑝 ∈ 𝐶) → 𝑝 ∈ 𝐴)
127	126	ex 418	. 2 ⊢ (𝐷 ∈ Fin → (𝑝 ∈ 𝐶 → 𝑝 ∈ 𝐴))
128	127	ssrdv 3919	1 ⊢ (𝐷 ∈ Fin → 𝐶 ⊆ 𝐴)

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2147 ≠ wne 2959 {crab 3416 Vcvv 3454 ⊆ wss 3900 ∩ cin 4092 ∪ cun 4152 {csn 4588 {cpr 4590 {ctp 4592 class class class wbr 5106 ^◡ccnv 5654 dom cdm 5655 ran crn 5656 “ cima 5658 ∘ ccom 5659 Fn wfn 6553 ⟶wf 6554 ⟶1-1wf1 6555 ‘cfv 6558 (class class class)co 7443 2_oc2o 8498 ≈ cen 8998 Fincfn 9001 0cc0 11227 1c1 11228 · cmul 11232 +∞cpnf 11367 -cneg 11569 2c2 12424 3c3 12425 ℕ₀cn0 12633 ..^cfzo 13815 ♯chash 14501 Word cword 14685 ⟨“cs2 15020 ⟨“cs3 15021 Basecbs 17416 +_gcplusg 17457 SymGrpcsymg 19613 pmTrspcpmtr 19685 pmSgncpsgn 19733 pmEvencevpm 19734 toCycctocyc 33737

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5235 ax-sep 5252 ax-nul 5263 ax-pow 5331 ax-pr 5395 ax-un 7775 ax-cnex 11283 ax-resscn 11284 ax-1cn 11285 ax-icn 11286 ax-addcl 11287 ax-addrcl 11288 ax-mulcl 11289 ax-mulrcl 11290 ax-mulcom 11291 ax-addass 11292 ax-mulass 11293 ax-distr 11294 ax-i2m1 11295 ax-1ne0 11296 ax-1rid 11297 ax-rnegex 11298 ax-rrecex 11299 ax-cnre 11300 ax-pre-lttri 11301 ax-pre-lttrn 11302 ax-pre-ltadd 11303 ax-pre-mulgt0 11304 ax-pre-sup 11305 ax-addf 11306 ax-mulf 11307

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-xor 1542 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4839 df-ot 4862 df-uni 4871 df-int 4911 df-iun 4956 df-iin 4957 df-br 5107 df-opab 5171 df-mpt 5190 df-tr 5216 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-se 5609 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6322 df-ord 6383 df-on 6384 df-lim 6385 df-suc 6386 df-iota 6512 df-fun 6560 df-fn 6561 df-f 6562 df-f1 6563 df-fo 6564 df-f1o 6565 df-fv 6566 df-isom 6567 df-riota 7400 df-ov 7446 df-oprab 7447 df-mpo 7448 df-om 7902 df-1st 8025 df-2nd 8026 df-tpos 8271 df-frecs 8327 df-wrecs 8358 df-recs 8407 df-rdg 8446 df-1o 8504 df-2o 8505 df-er 8745 df-map 8877 df-en 9002 df-dom 9003 df-sdom 9004 df-fin 9005 df-sup 9461 df-inf 9462 df-card 10047 df-pnf 11372 df-mnf 11373 df-xr 11374 df-ltxr 11375 df-le 11376 df-sub 11570 df-neg 11571 df-div 12001 df-nn 12363 df-2 12432 df-3 12433 df-4 12434 df-5 12435 df-6 12436 df-7 12437 df-8 12438 df-9 12439 df-n0 12634 df-xnn0 12707 df-z 12721 df-dec 12842 df-uz 12993 df-rp 13148 df-fz 13667 df-fzo 13816 df-fl 13959 df-mod 14037 df-seq 14172 df-exp 14232 df-hash 14502 df-word 14686 df-lsw 14735 df-concat 14743 df-s1 14770 df-substr 14817 df-pfx 14849 df-splice 14927 df-reverse 14936 df-csh 14968 df-s2 15027 df-s3 15028 df-struct 17354 df-sets 17371 df-slot 17389 df-ndx 17401 df-base 17417 df-ress 17438 df-plusg 17470 df-mulr 17471 df-starv 17472 df-tset 17476 df-ple 17477 df-ds 17479 df-unif 17480 df-0g 17641 df-gsum 17642 df-mre 17785 df-mrc 17786 df-acs 17788 df-mgm 18845 df-sgrp 18937 df-mnd 18953 df-mhm 19007 df-submnd 19008 df-efmnd 19094 df-grp 19176 df-minusg 19177 df-subg 19362 df-ghm 19457 df-gim 19502 df-oppg 19590 df-symg 19614 df-pmtr 19686 df-psgn 19735 df-evpm 19736 df-cmn 20026 df-abl 20027 df-mgp 20391 df-rng 20405 df-ur 20438 df-ring 20491 df-cring 20492 df-oppr 20597 df-dvdsr 20617 df-unit 20618 df-invr 20648 df-dvr 20661 df-drng 21012 df-cnfld 21709 df-tocyc 33738

This theorem is used by: cyc3genpm 33783

W3C validator