psgnunilem5

Description: Lemma for psgnuni . It is impossible to shift a transposition off the end because if the active transposition is at the right end, it is the only transposition moving A in contradiction to this being a representation of the identity. (Contributed by Stefan O'Rear, 25-Aug-2015) (Revised by Mario Carneiro, 28-Feb-2016) (Proof shortened by AV, 12-Oct-2022)

	Ref	Expression
Hypotheses	psgnunilem2.g	$⊢ G = SymGrp (D)$
	psgnunilem2.t	$⊢ T = ran pmTrsp (D)$
	psgnunilem2.d	$⊢ φ \to D \in V$
	psgnunilem2.w	$⊢ φ \to W \in Word T$
	psgnunilem2.id	$⊢ φ \to \sum_{G} W = {I ↾}_{D}$
	psgnunilem2.l	$⊢ φ \to \|W\| = L$
	psgnunilem2.ix	$⊢ φ \to I \in (0 ..^L)$
	psgnunilem2.a	$⊢ φ \to A \in dom (W (I) ∖ I)$
	psgnunilem2.al	$⊢ φ \to \forall k \in (0 ..^I) \neg A \in dom (W (k) ∖ I)$
Assertion	psgnunilem5	$⊢ φ \to I + 1 \in (0 ..^L)$

Proof

Step	Hyp	Ref	Expression
1		psgnunilem2.g	$⊢ G = SymGrp (D)$
2		psgnunilem2.t	$⊢ T = ran pmTrsp (D)$
3		psgnunilem2.d	$⊢ φ \to D \in V$
4		psgnunilem2.w	$⊢ φ \to W \in Word T$
5		psgnunilem2.id	$⊢ φ \to \sum_{G} W = {I ↾}_{D}$
6		psgnunilem2.l	$⊢ φ \to \|W\| = L$
7		psgnunilem2.ix	$⊢ φ \to I \in (0 ..^L)$
8		psgnunilem2.a	$⊢ φ \to A \in dom (W (I) ∖ I)$
9		psgnunilem2.al	$⊢ φ \to \forall k \in (0 ..^I) \neg A \in dom (W (k) ∖ I)$
10		noel	$⊢ \neg A \in \emptyset$
11	5	difeq1d	$⊢ φ \to (\sum_{G}, W) ∖ I = ({I ↾}_{D}) ∖ I$
12	11	dmeqd	$⊢ φ \to dom ((\sum_{G}, W) ∖ I) = dom (({I ↾}_{D}) ∖ I)$
13		resss	$⊢ {I ↾}_{D} \subseteq I$
14		ssdif0	$⊢ {I ↾}_{D} \subseteq I \leftrightarrow ({I ↾}_{D}) ∖ I = \emptyset$
15	13 14	mpbi	$⊢ ({I ↾}_{D}) ∖ I = \emptyset$
16	15	dmeqi	$⊢ dom (({I ↾}_{D}) ∖ I) = dom \emptyset$
17		dm0	$⊢ dom \emptyset = \emptyset$
18	16 17	eqtri	$⊢ dom (({I ↾}_{D}) ∖ I) = \emptyset$
19	12 18	eqtrdi	$⊢ φ \to dom ((\sum_{G}, W) ∖ I) = \emptyset$
20	19	eleq2d	$⊢ φ \to (A \in dom ((\sum_{G}, W) ∖ I) \leftrightarrow A \in \emptyset)$
21	10 20	mtbiri	$⊢ φ \to \neg A \in dom ((\sum_{G}, W) ∖ I)$
22	1	symggrp	$⊢ D \in V \to G \in Grp$
23		grpmnd	$⊢ G \in Grp \to G \in Mnd$
24	3 22 23	3syl	$⊢ φ \to G \in Mnd$
25		eqid	$⊢ {Base}_{G} = {Base}_{G}$
26	2 1 25	symgtrf	$⊢ T \subseteq {Base}_{G}$
27		sswrd	$⊢ T \subseteq {Base}_{G} \to Word T \subseteq Word {Base}_{G}$
28	26 27	mp1i	$⊢ φ \to Word T \subseteq Word {Base}_{G}$
29	28 4	sseldd	$⊢ φ \to W \in Word {Base}_{G}$
30		pfxcl	$⊢ W \in Word {Base}_{G} \to W prefix I \in Word {Base}_{G}$
31	29 30	syl	$⊢ φ \to W prefix I \in Word {Base}_{G}$
32	25	gsumwcl	$⊢ (G \in Mnd \land W prefix I \in Word {Base}_{G}) \to \sum_{G} (W prefix I) \in {Base}_{G}$
33	24 31 32	syl2anc	$⊢ φ \to \sum_{G} (W prefix I) \in {Base}_{G}$
34	1 25	symgbasf1o	$⊢ \sum_{G} (W prefix I) \in {Base}_{G} \to (\sum_{G}, (W prefix I)) : D \underset{1-1 onto}{⟶} D$
35	33 34	syl	$⊢ φ \to (\sum_{G}, (W prefix I)) : D \underset{1-1 onto}{⟶} D$
36	35	adantr	$⊢ (φ \land I + 1 = L) \to (\sum_{G}, (W prefix I)) : D \underset{1-1 onto}{⟶} D$
37		wrdf	$⊢ W \in Word T \to W : (0 ..^\|W\|) ⟶ T$
38	4 37	syl	$⊢ φ \to W : (0 ..^\|W\|) ⟶ T$
39	6	oveq2d	$⊢ φ \to (0 ..^\|W\|) = (0 ..^L)$
40	7 39	eleqtrrd	$⊢ φ \to I \in (0 ..^\|W\|)$
41	38 40	ffvelrnd	$⊢ φ \to W (I) \in T$
42	26 41	sseldi	$⊢ φ \to W (I) \in {Base}_{G}$
43	1 25	symgbasf1o	$⊢ W (I) \in {Base}_{G} \to W (I) : D \underset{1-1 onto}{⟶} D$
44	42 43	syl	$⊢ φ \to W (I) : D \underset{1-1 onto}{⟶} D$
45	44	adantr	$⊢ (φ \land I + 1 = L) \to W (I) : D \underset{1-1 onto}{⟶} D$
46	1 25	symgsssg	$⊢ D \in V \to \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\} \in SubGrp (G)$
47		subgsubm	$⊢ \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\} \in SubGrp (G) \to \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\} \in SubMnd (G)$
48	3 46 47	3syl	$⊢ φ \to \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\} \in SubMnd (G)$
49		fzossfz	$⊢ (0 ..^L) \subseteq (0 \dots L)$
50	49 7	sseldi	$⊢ φ \to I \in (0 \dots L)$
51	6	oveq2d	$⊢ φ \to (0 \dots \|W\|) = (0 \dots L)$
52	50 51	eleqtrrd	$⊢ φ \to I \in (0 \dots \|W\|)$
53		pfxmpt	$⊢ (W \in Word T \land I \in (0 \dots \|W\|)) \to W prefix I = (s \in (0 ..^I) ⟼ W (s))$
54	4 52 53	syl2anc	$⊢ φ \to W prefix I = (s \in (0 ..^I) ⟼ W (s))$
55		difeq1	$⊢ j = W (s) \to j ∖ I = W (s) ∖ I$
56	55	dmeqd	$⊢ j = W (s) \to dom (j ∖ I) = dom (W (s) ∖ I)$
57	56	sseq1d	$⊢ j = W (s) \to (dom (j ∖ I) \subseteq V ∖ \{A\} \leftrightarrow dom (W (s) ∖ I) \subseteq V ∖ \{A\})$
58		disj2	$⊢ dom (W (s) ∖ I) \cap \{A\} = \emptyset \leftrightarrow dom (W (s) ∖ I) \subseteq V ∖ \{A\}$
59		disjsn	$⊢ dom (W (s) ∖ I) \cap \{A\} = \emptyset \leftrightarrow \neg A \in dom (W (s) ∖ I)$
60	58 59	bitr3i	$⊢ dom (W (s) ∖ I) \subseteq V ∖ \{A\} \leftrightarrow \neg A \in dom (W (s) ∖ I)$
61	57 60	bitrdi	$⊢ j = W (s) \to (dom (j ∖ I) \subseteq V ∖ \{A\} \leftrightarrow \neg A \in dom (W (s) ∖ I))$
62		elfzuz3	$⊢ I \in (0 \dots L) \to L \in ℤ_{\geq I}$
63	50 62	syl	$⊢ φ \to L \in ℤ_{\geq I}$
64	6 63	eqeltrd	$⊢ φ \to \|W\| \in ℤ_{\geq I}$
65		fzoss2	$⊢ \|W\| \in ℤ_{\geq I} \to (0 ..^I) \subseteq (0 ..^\|W\|)$
66	64 65	syl	$⊢ φ \to (0 ..^I) \subseteq (0 ..^\|W\|)$
67	66	sselda	$⊢ (φ \land s \in (0 ..^I)) \to s \in (0 ..^\|W\|)$
68	38	ffvelrnda	$⊢ (φ \land s \in (0 ..^\|W\|)) \to W (s) \in T$
69	26 68	sseldi	$⊢ (φ \land s \in (0 ..^\|W\|)) \to W (s) \in {Base}_{G}$
70	67 69	syldan	$⊢ (φ \land s \in (0 ..^I)) \to W (s) \in {Base}_{G}$
71		fveq2	$⊢ k = s \to W (k) = W (s)$
72	71	difeq1d	$⊢ k = s \to W (k) ∖ I = W (s) ∖ I$
73	72	dmeqd	$⊢ k = s \to dom (W (k) ∖ I) = dom (W (s) ∖ I)$
74	73	eleq2d	$⊢ k = s \to (A \in dom (W (k) ∖ I) \leftrightarrow A \in dom (W (s) ∖ I))$
75	74	notbid	$⊢ k = s \to (\neg A \in dom (W (k) ∖ I) \leftrightarrow \neg A \in dom (W (s) ∖ I))$
76	75	cbvralvw	$⊢ \forall k \in (0 ..^I) \neg A \in dom (W (k) ∖ I) \leftrightarrow \forall s \in (0 ..^I) \neg A \in dom (W (s) ∖ I)$
77	9 76	sylib	$⊢ φ \to \forall s \in (0 ..^I) \neg A \in dom (W (s) ∖ I)$
78	77	r19.21bi	$⊢ (φ \land s \in (0 ..^I)) \to \neg A \in dom (W (s) ∖ I)$
79	61 70 78	elrabd	$⊢ (φ \land s \in (0 ..^I)) \to W (s) \in \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\}$
80	54 79	fmpt3d	$⊢ φ \to (W prefix I) : (0 ..^I) ⟶ \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\}$
81	80	adantr	$⊢ (φ \land I + 1 = L) \to (W prefix I) : (0 ..^I) ⟶ \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\}$
82		iswrdi	$⊢ (W prefix I) : (0 ..^I) ⟶ \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\} \to W prefix I \in Word \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\}$
83	81 82	syl	$⊢ (φ \land I + 1 = L) \to W prefix I \in Word \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\}$
84		gsumwsubmcl	$⊢ (\{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\} \in SubMnd (G) \land W prefix I \in Word \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\}) \to \sum_{G} (W prefix I) \in \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\}$
85	48 83 84	syl2an2r	$⊢ (φ \land I + 1 = L) \to \sum_{G} (W prefix I) \in \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\}$
86		difeq1	$⊢ j = \sum_{G} (W prefix I) \to j ∖ I = (\sum_{G}, (W prefix I)) ∖ I$
87	86	dmeqd	$⊢ j = \sum_{G} (W prefix I) \to dom (j ∖ I) = dom ((\sum_{G}, (W prefix I)) ∖ I)$
88	87	sseq1d	$⊢ j = \sum_{G} (W prefix I) \to (dom (j ∖ I) \subseteq V ∖ \{A\} \leftrightarrow dom ((\sum_{G}, (W prefix I)) ∖ I) \subseteq V ∖ \{A\})$
89	88	elrab	$⊢ \sum_{G} (W prefix I) \in \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\} \leftrightarrow (\sum_{G} (W prefix I) \in {Base}_{G} \land dom ((\sum_{G}, (W prefix I)) ∖ I) \subseteq V ∖ \{A\})$
90	89	simprbi	$⊢ \sum_{G} (W prefix I) \in \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\} \to dom ((\sum_{G}, (W prefix I)) ∖ I) \subseteq V ∖ \{A\}$
91		disj2	$⊢ dom ((\sum_{G}, (W prefix I)) ∖ I) \cap \{A\} = \emptyset \leftrightarrow dom ((\sum_{G}, (W prefix I)) ∖ I) \subseteq V ∖ \{A\}$
92		disjsn	$⊢ dom ((\sum_{G}, (W prefix I)) ∖ I) \cap \{A\} = \emptyset \leftrightarrow \neg A \in dom ((\sum_{G}, (W prefix I)) ∖ I)$
93	91 92	bitr3i	$⊢ dom ((\sum_{G}, (W prefix I)) ∖ I) \subseteq V ∖ \{A\} \leftrightarrow \neg A \in dom ((\sum_{G}, (W prefix I)) ∖ I)$
94	90 93	sylib	$⊢ \sum_{G} (W prefix I) \in \{j \in {Base}_{G} \| dom (j ∖ I) \subseteq V ∖ \{A\}\} \to \neg A \in dom ((\sum_{G}, (W prefix I)) ∖ I)$
95	85 94	syl	$⊢ (φ \land I + 1 = L) \to \neg A \in dom ((\sum_{G}, (W prefix I)) ∖ I)$
96	8	adantr	$⊢ (φ \land I + 1 = L) \to A \in dom (W (I) ∖ I)$
97	95 96	jca	$⊢ (φ \land I + 1 = L) \to (\neg A \in dom ((\sum_{G}, (W prefix I)) ∖ I) \land A \in dom (W (I) ∖ I))$
98	97	olcd	$⊢ (φ \land I + 1 = L) \to ((A \in dom ((\sum_{G}, (W prefix I)) ∖ I) \land \neg A \in dom (W (I) ∖ I)) \lor (\neg A \in dom ((\sum_{G}, (W prefix I)) ∖ I) \land A \in dom (W (I) ∖ I)))$
99		excxor	$⊢ (A \in dom ((\sum_{G}, (W prefix I)) ∖ I) ⊻ A \in dom (W (I) ∖ I)) \leftrightarrow ((A \in dom ((\sum_{G}, (W prefix I)) ∖ I) \land \neg A \in dom (W (I) ∖ I)) \lor (\neg A \in dom ((\sum_{G}, (W prefix I)) ∖ I) \land A \in dom (W (I) ∖ I)))$
100	98 99	sylibr	$⊢ (φ \land I + 1 = L) \to (A \in dom ((\sum_{G}, (W prefix I)) ∖ I) ⊻ A \in dom (W (I) ∖ I))$
101		f1omvdco3	$⊢ ((\sum_{G}, (W prefix I)) : D \underset{1-1 onto}{⟶} D \land W (I) : D \underset{1-1 onto}{⟶} D \land (A \in dom ((\sum_{G}, (W prefix I)) ∖ I) ⊻ A \in dom (W (I) ∖ I))) \to A \in dom (((\sum_{G}, (W prefix I)) \circ W (I)) ∖ I)$
102	36 45 100 101	syl3anc	$⊢ (φ \land I + 1 = L) \to A \in dom (((\sum_{G}, (W prefix I)) \circ W (I)) ∖ I)$
103		elfzo0	$⊢ I \in (0 ..^L) \leftrightarrow (I \in ℕ_{0} \land L \in ℕ \land I < L)$
104	103	simp2bi	$⊢ I \in (0 ..^L) \to L \in ℕ$
105	7 104	syl	$⊢ φ \to L \in ℕ$
106	6 105	eqeltrd	$⊢ φ \to \|W\| \in ℕ$
107		wrdfin	$⊢ W \in Word T \to W \in Fin$
108		hashnncl	$⊢ W \in Fin \to (\|W\| \in ℕ \leftrightarrow W \neq \emptyset)$
109	4 107 108	3syl	$⊢ φ \to (\|W\| \in ℕ \leftrightarrow W \neq \emptyset)$
110	106 109	mpbid	$⊢ φ \to W \neq \emptyset$
111	110	adantr	$⊢ (φ \land I + 1 = L) \to W \neq \emptyset$
112		pfxlswccat	$⊢ (W \in Word T \land W \neq \emptyset) \to (W prefix (\|W\| - 1)) ++ ⟨“ lastS (W) ”⟩ = W$
113	112	eqcomd	$⊢ (W \in Word T \land W \neq \emptyset) \to W = (W prefix (\|W\| - 1)) ++ ⟨“ lastS (W) ”⟩$
114	4 111 113	syl2an2r	$⊢ (φ \land I + 1 = L) \to W = (W prefix (\|W\| - 1)) ++ ⟨“ lastS (W) ”⟩$
115	6	oveq1d	$⊢ φ \to \|W\| - 1 = L - 1$
116	115	adantr	$⊢ (φ \land I + 1 = L) \to \|W\| - 1 = L - 1$
117	105	nncnd	$⊢ φ \to L \in ℂ$
118		1cnd	$⊢ φ \to 1 \in ℂ$
119		elfzoelz	$⊢ I \in (0 ..^L) \to I \in ℤ$
120	7 119	syl	$⊢ φ \to I \in ℤ$
121	120	zcnd	$⊢ φ \to I \in ℂ$
122	117 118 121	subadd2d	$⊢ φ \to (L - 1 = I \leftrightarrow I + 1 = L)$
123	122	biimpar	$⊢ (φ \land I + 1 = L) \to L - 1 = I$
124	116 123	eqtrd	$⊢ (φ \land I + 1 = L) \to \|W\| - 1 = I$
125		oveq2	$⊢ \|W\| - 1 = I \to W prefix (\|W\| - 1) = W prefix I$
126	125	adantl	$⊢ (φ \land \|W\| - 1 = I) \to W prefix (\|W\| - 1) = W prefix I$
127		lsw	$⊢ W \in Word T \to lastS (W) = W (\|W\| - 1)$
128	4 127	syl	$⊢ φ \to lastS (W) = W (\|W\| - 1)$
129		fveq2	$⊢ \|W\| - 1 = I \to W (\|W\| - 1) = W (I)$
130	128 129	sylan9eq	$⊢ (φ \land \|W\| - 1 = I) \to lastS (W) = W (I)$
131	130	s1eqd	$⊢ (φ \land \|W\| - 1 = I) \to ⟨“ lastS (W) ”⟩ = ⟨“ W (I) ”⟩$
132	126 131	oveq12d	$⊢ (φ \land \|W\| - 1 = I) \to (W prefix (\|W\| - 1)) ++ ⟨“ lastS (W) ”⟩ = (W prefix I) ++ ⟨“ W (I) ”⟩$
133	124 132	syldan	$⊢ (φ \land I + 1 = L) \to (W prefix (\|W\| - 1)) ++ ⟨“ lastS (W) ”⟩ = (W prefix I) ++ ⟨“ W (I) ”⟩$
134	114 133	eqtrd	$⊢ (φ \land I + 1 = L) \to W = (W prefix I) ++ ⟨“ W (I) ”⟩$
135	134	oveq2d	$⊢ (φ \land I + 1 = L) \to \sum_{G} W = \sum_{G} ((W prefix I) ++ ⟨“ W (I) ”⟩)$
136	42	s1cld	$⊢ φ \to ⟨“ W (I) ”⟩ \in Word {Base}_{G}$
137		eqid	$⊢ +_{G} = +_{G}$
138	25 137	gsumccat	$⊢ (G \in Mnd \land W prefix I \in Word {Base}_{G} \land ⟨“ W (I) ”⟩ \in Word {Base}_{G}) \to \sum_{G} ((W prefix I) ++ ⟨“ W (I) ”⟩) = (\sum_{G}, (W prefix I)) +_{G} (\sum_{G}, ⟨“ W (I) ”⟩)$
139	24 31 136 138	syl3anc	$⊢ φ \to \sum_{G} ((W prefix I) ++ ⟨“ W (I) ”⟩) = (\sum_{G}, (W prefix I)) +_{G} (\sum_{G}, ⟨“ W (I) ”⟩)$
140	139	adantr	$⊢ (φ \land I + 1 = L) \to \sum_{G} ((W prefix I) ++ ⟨“ W (I) ”⟩) = (\sum_{G}, (W prefix I)) +_{G} (\sum_{G}, ⟨“ W (I) ”⟩)$
141	25	gsumws1	$⊢ W (I) \in {Base}_{G} \to \sum_{G} ⟨“ W (I) ”⟩ = W (I)$
142	42 141	syl	$⊢ φ \to \sum_{G} ⟨“ W (I) ”⟩ = W (I)$
143	142	oveq2d	$⊢ φ \to (\sum_{G}, (W prefix I)) +_{G} (\sum_{G}, ⟨“ W (I) ”⟩) = (\sum_{G}, (W prefix I)) +_{G} W (I)$
144	1 25 137	symgov	$⊢ (\sum_{G} (W prefix I) \in {Base}_{G} \land W (I) \in {Base}_{G}) \to (\sum_{G}, (W prefix I)) +_{G} W (I) = (\sum_{G}, (W prefix I)) \circ W (I)$
145	33 42 144	syl2anc	$⊢ φ \to (\sum_{G}, (W prefix I)) +_{G} W (I) = (\sum_{G}, (W prefix I)) \circ W (I)$
146	143 145	eqtrd	$⊢ φ \to (\sum_{G}, (W prefix I)) +_{G} (\sum_{G}, ⟨“ W (I) ”⟩) = (\sum_{G}, (W prefix I)) \circ W (I)$
147	146	adantr	$⊢ (φ \land I + 1 = L) \to (\sum_{G}, (W prefix I)) +_{G} (\sum_{G}, ⟨“ W (I) ”⟩) = (\sum_{G}, (W prefix I)) \circ W (I)$
148	135 140 147	3eqtrd	$⊢ (φ \land I + 1 = L) \to \sum_{G} W = (\sum_{G}, (W prefix I)) \circ W (I)$
149	148	difeq1d	$⊢ (φ \land I + 1 = L) \to (\sum_{G}, W) ∖ I = ((\sum_{G}, (W prefix I)) \circ W (I)) ∖ I$
150	149	dmeqd	$⊢ (φ \land I + 1 = L) \to dom ((\sum_{G}, W) ∖ I) = dom (((\sum_{G}, (W prefix I)) \circ W (I)) ∖ I)$
151	102 150	eleqtrrd	$⊢ (φ \land I + 1 = L) \to A \in dom ((\sum_{G}, W) ∖ I)$
152	21 151	mtand	$⊢ φ \to \neg I + 1 = L$
153		fzostep1	$⊢ I \in (0 ..^L) \to (I + 1 \in (0 ..^L) \lor I + 1 = L)$
154	7 153	syl	$⊢ φ \to (I + 1 \in (0 ..^L) \lor I + 1 = L)$
155	154	ord	$⊢ φ \to (\neg I + 1 \in (0 ..^L) \to I + 1 = L)$
156	152 155	mt3d	$⊢ φ \to I + 1 \in (0 ..^L)$

Metamath Proof Explorer

Theorem psgnunilem5

Proof