cyc3genpm

Description: The alternating group A is generated by 3-cycles. Property (a) of Lang p. 32 . (Contributed by Thierry Arnoux, 27-Sep-2023)

	Ref	Expression
Hypotheses	cyc3genpm.t	$⊢ C = M [{\|.\|}^{-1} [\{3\}]]$
	cyc3genpm.a	$⊢ A = pmEven (D)$
	cyc3genpm.s	$⊢ S = SymGrp (D)$
	cyc3genpm.n	$⊢ N = \|D\|$
	cyc3genpm.m	$⊢ M = toCyc (D)$
Assertion	cyc3genpm	$⊢ D \in Fin \to (Q \in A \leftrightarrow \exists w \in Word C Q = \sum_{S} w)$

Proof

Step	Hyp	Ref	Expression
1		cyc3genpm.t	$⊢ C = M [{\|.\|}^{-1} [\{3\}]]$
2		cyc3genpm.a	$⊢ A = pmEven (D)$
3		cyc3genpm.s	$⊢ S = SymGrp (D)$
4		cyc3genpm.n	$⊢ N = \|D\|$
5		cyc3genpm.m	$⊢ M = toCyc (D)$
6		simplr	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to v \in Word ran pmTrsp (D)$
7		lencl	$⊢ v \in Word ran pmTrsp (D) \to \|v\| \in ℕ_{0}$
8	7	ad2antlr	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to \|v\| \in ℕ_{0}$
9	8	nn0zd	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to \|v\| \in ℤ$
10		simpr	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to Q = \sum_{S} v$
11	10	fveq2d	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to pmSgn (D) (Q) = pmSgn (D) (\sum_{S} v)$
12		simplll	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to D \in Fin$
13		simpllr	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to Q \in A$
14	13 2	eleqtrdi	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to Q \in pmEven (D)$
15		eqid	$⊢ {Base}_{S} = {Base}_{S}$
16		eqid	$⊢ pmSgn (D) = pmSgn (D)$
17	3 15 16	psgnevpm	$⊢ (D \in Fin \land Q \in pmEven (D)) \to pmSgn (D) (Q) = 1$
18	12 14 17	syl2anc	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to pmSgn (D) (Q) = 1$
19		eqid	$⊢ ran pmTrsp (D) = ran pmTrsp (D)$
20	3 19 16	psgnvalii	$⊢ (D \in Fin \land v \in Word ran pmTrsp (D)) \to pmSgn (D) (\sum_{S} v) = {(- 1)}^{\|v\|}$
21	12 6 20	syl2anc	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to pmSgn (D) (\sum_{S} v) = {(- 1)}^{\|v\|}$
22	11 18 21	3eqtr3rd	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to {(- 1)}^{\|v\|} = 1$
23		m1exp1	$⊢ \|v\| \in ℤ \to ({(- 1)}^{\|v\|} = 1 \leftrightarrow 2 ∥ \|v\|)$
24	23	biimpa	$⊢ (\|v\| \in ℤ \land {(- 1)}^{\|v\|} = 1) \to 2 ∥ \|v\|$
25	9 22 24	syl2anc	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to 2 ∥ \|v\|$
26		oveq2	$⊢ x = \emptyset \to \sum_{S} x = \sum_{S} \emptyset$
27	26	eqeq1d	$⊢ x = \emptyset \to (\sum_{S} x = \sum_{S} w \leftrightarrow \sum_{S} \emptyset = \sum_{S} w)$
28	27	rexbidv	$⊢ x = \emptyset \to (\exists w \in Word C \sum_{S} x = \sum_{S} w \leftrightarrow \exists w \in Word C \sum_{S} \emptyset = \sum_{S} w)$
29	28	imbi2d	$⊢ x = \emptyset \to ((D \in Fin \to \exists w \in Word C \sum_{S} x = \sum_{S} w) \leftrightarrow (D \in Fin \to \exists w \in Word C \sum_{S} \emptyset = \sum_{S} w))$
30		oveq2	$⊢ x = u \to \sum_{S} x = \sum_{S} u$
31	30	eqeq1d	$⊢ x = u \to (\sum_{S} x = \sum_{S} w \leftrightarrow \sum_{S} u = \sum_{S} w)$
32	31	rexbidv	$⊢ x = u \to (\exists w \in Word C \sum_{S} x = \sum_{S} w \leftrightarrow \exists w \in Word C \sum_{S} u = \sum_{S} w)$
33	32	imbi2d	$⊢ x = u \to ((D \in Fin \to \exists w \in Word C \sum_{S} x = \sum_{S} w) \leftrightarrow (D \in Fin \to \exists w \in Word C \sum_{S} u = \sum_{S} w))$
34		oveq2	$⊢ x = u ++ ⟨“ i j ”⟩ \to \sum_{S} x = \sum_{S} (u ++ ⟨“ i j ”⟩)$
35	34	eqeq1d	$⊢ x = u ++ ⟨“ i j ”⟩ \to (\sum_{S} x = \sum_{S} w \leftrightarrow \sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} w)$
36	35	rexbidv	$⊢ x = u ++ ⟨“ i j ”⟩ \to (\exists w \in Word C \sum_{S} x = \sum_{S} w \leftrightarrow \exists w \in Word C \sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} w)$
37	36	imbi2d	$⊢ x = u ++ ⟨“ i j ”⟩ \to ((D \in Fin \to \exists w \in Word C \sum_{S} x = \sum_{S} w) \leftrightarrow (D \in Fin \to \exists w \in Word C \sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} w))$
38		oveq2	$⊢ x = v \to \sum_{S} x = \sum_{S} v$
39	38	eqeq1d	$⊢ x = v \to (\sum_{S} x = \sum_{S} w \leftrightarrow \sum_{S} v = \sum_{S} w)$
40	39	rexbidv	$⊢ x = v \to (\exists w \in Word C \sum_{S} x = \sum_{S} w \leftrightarrow \exists w \in Word C \sum_{S} v = \sum_{S} w)$
41	40	imbi2d	$⊢ x = v \to ((D \in Fin \to \exists w \in Word C \sum_{S} x = \sum_{S} w) \leftrightarrow (D \in Fin \to \exists w \in Word C \sum_{S} v = \sum_{S} w))$
42		wrd0	$⊢ \emptyset \in Word C$
43	42	a1i	$⊢ D \in Fin \to \emptyset \in Word C$
44		simpr	$⊢ (D \in Fin \land w = \emptyset) \to w = \emptyset$
45	44	oveq2d	$⊢ (D \in Fin \land w = \emptyset) \to \sum_{S} w = \sum_{S} \emptyset$
46	45	eqeq2d	$⊢ (D \in Fin \land w = \emptyset) \to (\sum_{S} \emptyset = \sum_{S} w \leftrightarrow \sum_{S} \emptyset = \sum_{S} \emptyset)$
47		eqidd	$⊢ D \in Fin \to \sum_{S} \emptyset = \sum_{S} \emptyset$
48	43 46 47	rspcedvd	$⊢ D \in Fin \to \exists w \in Word C \sum_{S} \emptyset = \sum_{S} w$
49		ccatcl	$⊢ (v \in Word C \land c \in Word C) \to v ++ c \in Word C$
50	49	ad5ant24	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to v ++ c \in Word C$
51		oveq2	$⊢ w = v ++ c \to \sum_{S} w = \sum_{S} (v ++ c)$
52	51	eqeq2d	$⊢ w = v ++ c \to (\sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} w \leftrightarrow \sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} (v ++ c))$
53	52	adantl	$⊢ ((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \land w = v ++ c) \to (\sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} w \leftrightarrow \sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} (v ++ c))$
54		simpllr	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to \sum_{S} u = \sum_{S} v$
55		simpllr	$⊢ (((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \to D \in Fin$
56	55	ad2antrr	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to D \in Fin$
57	3	symggrp	$⊢ D \in Fin \to S \in Grp$
58		grpmnd	$⊢ S \in Grp \to S \in Mnd$
59	56 57 58	3syl	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to S \in Mnd$
60	19 3 15	symgtrf	$⊢ ran pmTrsp (D) \subseteq {Base}_{S}$
61	60	a1i	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to ran pmTrsp (D) \subseteq {Base}_{S}$
62		simp-5r	$⊢ (((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \to i \in ran pmTrsp (D)$
63	62	ad2antrr	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to i \in ran pmTrsp (D)$
64	61 63	sseldd	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to i \in {Base}_{S}$
65		simp-6r	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to j \in ran pmTrsp (D)$
66	61 65	sseldd	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to j \in {Base}_{S}$
67		eqid	$⊢ +_{S} = +_{S}$
68	15 67	gsumws2	$⊢ (S \in Mnd \land i \in {Base}_{S} \land j \in {Base}_{S}) \to \sum_{S} ⟨“ i j ”⟩ = i +_{S} j$
69	59 64 66 68	syl3anc	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to \sum_{S} ⟨“ i j ”⟩ = i +_{S} j$
70		simpr	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to i +_{S} j = \sum_{S} c$
71	69 70	eqtrd	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to \sum_{S} ⟨“ i j ”⟩ = \sum_{S} c$
72	54 71	oveq12d	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to (\sum_{S}, u) +_{S} (\sum_{S}, ⟨“ i j ”⟩) = (\sum_{S}, v) +_{S} (\sum_{S}, c)$
73		sswrd	$⊢ ran pmTrsp (D) \subseteq {Base}_{S} \to Word ran pmTrsp (D) \subseteq Word {Base}_{S}$
74	61 73	syl	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to Word ran pmTrsp (D) \subseteq Word {Base}_{S}$
75		simp-7l	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to u \in Word ran pmTrsp (D)$
76	74 75	sseldd	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to u \in Word {Base}_{S}$
77	64 66	s2cld	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to ⟨“ i j ”⟩ \in Word {Base}_{S}$
78	15 67	gsumccat	$⊢ (S \in Mnd \land u \in Word {Base}_{S} \land ⟨“ i j ”⟩ \in Word {Base}_{S}) \to \sum_{S} (u ++ ⟨“ i j ”⟩) = (\sum_{S}, u) +_{S} (\sum_{S}, ⟨“ i j ”⟩)$
79	59 76 77 78	syl3anc	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to \sum_{S} (u ++ ⟨“ i j ”⟩) = (\sum_{S}, u) +_{S} (\sum_{S}, ⟨“ i j ”⟩)$
80	5	imaeq1i	$⊢ M [{\|.\|}^{-1} [\{3\}]] = toCyc (D) [{\|.\|}^{-1} [\{3\}]]$
81	1 80	eqtri	$⊢ C = toCyc (D) [{\|.\|}^{-1} [\{3\}]]$
82	81 2	cyc3evpm	$⊢ D \in Fin \to C \subseteq A$
83	3 15	evpmss	$⊢ pmEven (D) \subseteq {Base}_{S}$
84	2 83	eqsstri	$⊢ A \subseteq {Base}_{S}$
85	82 84	sstrdi	$⊢ D \in Fin \to C \subseteq {Base}_{S}$
86		sswrd	$⊢ C \subseteq {Base}_{S} \to Word C \subseteq Word {Base}_{S}$
87	56 85 86	3syl	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to Word C \subseteq Word {Base}_{S}$
88		simp-4r	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to v \in Word C$
89	87 88	sseldd	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to v \in Word {Base}_{S}$
90		simplr	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to c \in Word C$
91	87 90	sseldd	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to c \in Word {Base}_{S}$
92	15 67	gsumccat	$⊢ (S \in Mnd \land v \in Word {Base}_{S} \land c \in Word {Base}_{S}) \to \sum_{S} (v ++ c) = (\sum_{S}, v) +_{S} (\sum_{S}, c)$
93	59 89 91 92	syl3anc	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to \sum_{S} (v ++ c) = (\sum_{S}, v) +_{S} (\sum_{S}, c)$
94	72 79 93	3eqtr4d	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to \sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} (v ++ c)$
95	50 53 94	rspcedvd	$⊢ (((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land c \in Word C) \land i +_{S} j = \sum_{S} c) \to \exists w \in Word C \sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} w$
96		simp-6r	$⊢ (((((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \land g \in D) \land h \in D) \land (g \neq h \land j = M (⟨“ g h ”⟩))) \to e \in D$
97		simp-5r	$⊢ (((((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \land g \in D) \land h \in D) \land (g \neq h \land j = M (⟨“ g h ”⟩))) \to f \in D$
98		simpllr	$⊢ (((((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \land g \in D) \land h \in D) \land (g \neq h \land j = M (⟨“ g h ”⟩))) \to g \in D$
99		simplr	$⊢ (((((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \land g \in D) \land h \in D) \land (g \neq h \land j = M (⟨“ g h ”⟩))) \to h \in D$
100		simp-4r	$⊢ (((((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \land g \in D) \land h \in D) \land (g \neq h \land j = M (⟨“ g h ”⟩))) \to (e \neq f \land i = M (⟨“ e f ”⟩))$
101	100	simprd	$⊢ (((((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \land g \in D) \land h \in D) \land (g \neq h \land j = M (⟨“ g h ”⟩))) \to i = M (⟨“ e f ”⟩)$
102		simprr	$⊢ (((((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \land g \in D) \land h \in D) \land (g \neq h \land j = M (⟨“ g h ”⟩))) \to j = M (⟨“ g h ”⟩)$
103	55	ad6antr	$⊢ (((((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \land g \in D) \land h \in D) \land (g \neq h \land j = M (⟨“ g h ”⟩))) \to D \in Fin$
104	100	simpld	$⊢ (((((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \land g \in D) \land h \in D) \land (g \neq h \land j = M (⟨“ g h ”⟩))) \to e \neq f$
105		simprl	$⊢ (((((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \land g \in D) \land h \in D) \land (g \neq h \land j = M (⟨“ g h ”⟩))) \to g \neq h$
106	1 2 3 4 5 67 96 97 98 99 101 102 103 104 105	cyc3genpmlem	$⊢ (((((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \land g \in D) \land h \in D) \land (g \neq h \land j = M (⟨“ g h ”⟩))) \to \exists c \in Word C i +_{S} j = \sum_{S} c$
107		simp-6r	$⊢ ((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \to D \in Fin$
108		simp-7r	$⊢ ((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \to j \in ran pmTrsp (D)$
109	19 5	trsp2cyc	$⊢ (D \in Fin \land j \in ran pmTrsp (D)) \to \exists g \in D \exists h \in D (g \neq h \land j = M (⟨“ g h ”⟩))$
110	107 108 109	syl2anc	$⊢ ((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \to \exists g \in D \exists h \in D (g \neq h \land j = M (⟨“ g h ”⟩))$
111	106 110	r19.29vva	$⊢ ((((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \land e \in D) \land f \in D) \land (e \neq f \land i = M (⟨“ e f ”⟩))) \to \exists c \in Word C i +_{S} j = \sum_{S} c$
112	19 5	trsp2cyc	$⊢ (D \in Fin \land i \in ran pmTrsp (D)) \to \exists e \in D \exists f \in D (e \neq f \land i = M (⟨“ e f ”⟩))$
113	55 62 112	syl2anc	$⊢ (((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \to \exists e \in D \exists f \in D (e \neq f \land i = M (⟨“ e f ”⟩))$
114	111 113	r19.29vva	$⊢ (((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \to \exists c \in Word C i +_{S} j = \sum_{S} c$
115	95 114	r19.29a	$⊢ (((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \to \exists w \in Word C \sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} w$
116	115	adantl3r	$⊢ ((((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land (D \in Fin \to \exists w \in Word C \sum_{S} u = \sum_{S} w)) \land D \in Fin) \land v \in Word C) \land \sum_{S} u = \sum_{S} v) \to \exists w \in Word C \sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} w$
117		simpr	$⊢ ((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land (D \in Fin \to \exists w \in Word C \sum_{S} u = \sum_{S} w)) \land D \in Fin) \to D \in Fin$
118		simplr	$⊢ ((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land (D \in Fin \to \exists w \in Word C \sum_{S} u = \sum_{S} w)) \land D \in Fin) \to (D \in Fin \to \exists w \in Word C \sum_{S} u = \sum_{S} w)$
119	117 118	mpd	$⊢ ((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land (D \in Fin \to \exists w \in Word C \sum_{S} u = \sum_{S} w)) \land D \in Fin) \to \exists w \in Word C \sum_{S} u = \sum_{S} w$
120		oveq2	$⊢ v = w \to \sum_{S} v = \sum_{S} w$
121	120	eqeq2d	$⊢ v = w \to (\sum_{S} u = \sum_{S} v \leftrightarrow \sum_{S} u = \sum_{S} w)$
122	121	cbvrexvw	$⊢ \exists v \in Word C \sum_{S} u = \sum_{S} v \leftrightarrow \exists w \in Word C \sum_{S} u = \sum_{S} w$
123	119 122	sylibr	$⊢ ((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land (D \in Fin \to \exists w \in Word C \sum_{S} u = \sum_{S} w)) \land D \in Fin) \to \exists v \in Word C \sum_{S} u = \sum_{S} v$
124	116 123	r19.29a	$⊢ ((((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land (D \in Fin \to \exists w \in Word C \sum_{S} u = \sum_{S} w)) \land D \in Fin) \to \exists w \in Word C \sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} w$
125	124	ex	$⊢ (((u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D)) \land j \in ran pmTrsp (D)) \land (D \in Fin \to \exists w \in Word C \sum_{S} u = \sum_{S} w)) \to (D \in Fin \to \exists w \in Word C \sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} w)$
126	125	ex3	$⊢ (u \in Word ran pmTrsp (D) \land i \in ran pmTrsp (D) \land j \in ran pmTrsp (D)) \to ((D \in Fin \to \exists w \in Word C \sum_{S} u = \sum_{S} w) \to (D \in Fin \to \exists w \in Word C \sum_{S} (u ++ ⟨“ i j ”⟩) = \sum_{S} w))$
127	29 33 37 41 48 126	wrdt2ind	$⊢ (v \in Word ran pmTrsp (D) \land 2 ∥ \|v\|) \to (D \in Fin \to \exists w \in Word C \sum_{S} v = \sum_{S} w)$
128	127	imp	$⊢ ((v \in Word ran pmTrsp (D) \land 2 ∥ \|v\|) \land D \in Fin) \to \exists w \in Word C \sum_{S} v = \sum_{S} w$
129	6 25 12 128	syl21anc	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to \exists w \in Word C \sum_{S} v = \sum_{S} w$
130	10	eqeq1d	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to (Q = \sum_{S} w \leftrightarrow \sum_{S} v = \sum_{S} w)$
131	130	rexbidv	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to (\exists w \in Word C Q = \sum_{S} w \leftrightarrow \exists w \in Word C \sum_{S} v = \sum_{S} w)$
132	129 131	mpbird	$⊢ (((D \in Fin \land Q \in A) \land v \in Word ran pmTrsp (D)) \land Q = \sum_{S} v) \to \exists w \in Word C Q = \sum_{S} w$
133	84	sseli	$⊢ Q \in A \to Q \in {Base}_{S}$
134	3 15 19	psgnfitr	$⊢ D \in Fin \to (Q \in {Base}_{S} \leftrightarrow \exists v \in Word ran pmTrsp (D) Q = \sum_{S} v)$
135	134	biimpa	$⊢ (D \in Fin \land Q \in {Base}_{S}) \to \exists v \in Word ran pmTrsp (D) Q = \sum_{S} v$
136	133 135	sylan2	$⊢ (D \in Fin \land Q \in A) \to \exists v \in Word ran pmTrsp (D) Q = \sum_{S} v$
137	132 136	r19.29a	$⊢ (D \in Fin \land Q \in A) \to \exists w \in Word C Q = \sum_{S} w$
138		simpr	$⊢ ((D \in Fin \land w \in Word C) \land Q = \sum_{S} w) \to Q = \sum_{S} w$
139	3	altgnsg	$⊢ D \in Fin \to pmEven (D) \in NrmSGrp (S)$
140	2 139	eqeltrid	$⊢ D \in Fin \to A \in NrmSGrp (S)$
141		nsgsubg	$⊢ A \in NrmSGrp (S) \to A \in SubGrp (S)$
142		subgsubm	$⊢ A \in SubGrp (S) \to A \in SubMnd (S)$
143	140 141 142	3syl	$⊢ D \in Fin \to A \in SubMnd (S)$
144	143	adantr	$⊢ (D \in Fin \land w \in Word C) \to A \in SubMnd (S)$
145		sswrd	$⊢ C \subseteq A \to Word C \subseteq Word A$
146	82 145	syl	$⊢ D \in Fin \to Word C \subseteq Word A$
147	146	sselda	$⊢ (D \in Fin \land w \in Word C) \to w \in Word A$
148		gsumwsubmcl	$⊢ (A \in SubMnd (S) \land w \in Word A) \to \sum_{S} w \in A$
149	144 147 148	syl2anc	$⊢ (D \in Fin \land w \in Word C) \to \sum_{S} w \in A$
150	149	adantr	$⊢ ((D \in Fin \land w \in Word C) \land Q = \sum_{S} w) \to \sum_{S} w \in A$
151	138 150	eqeltrd	$⊢ ((D \in Fin \land w \in Word C) \land Q = \sum_{S} w) \to Q \in A$
152	151	r19.29an	$⊢ (D \in Fin \land \exists w \in Word C Q = \sum_{S} w) \to Q \in A$
153	137 152	impbida	$⊢ D \in Fin \to (Q \in A \leftrightarrow \exists w \in Word C Q = \sum_{S} w)$

Metamath Proof Explorer

Theorem cyc3genpm

Proof