psgnunilem4

Description: Lemma for psgnuni . An odd-length representation of the identity is impossible, as it could be repeatedly shortened to a length of 1, but a length 1 permutation must be a transposition. (Contributed by Stefan O'Rear, 25-Aug-2015)

	Ref	Expression
Hypotheses	psgnunilem4.g	$⊢ G = SymGrp (D)$
	psgnunilem4.t	$⊢ T = ran pmTrsp (D)$
	psgnunilem4.d	$⊢ φ \to D \in V$
	psgnunilem4.w1	$⊢ φ \to W \in Word T$
	psgnunilem4.w2	$⊢ φ \to \sum_{G} W = {I ↾}_{D}$
Assertion	psgnunilem4	$⊢ φ \to {(- 1)}^{\|W\|} = 1$

Proof

Step	Hyp	Ref	Expression
1		psgnunilem4.g	$⊢ G = SymGrp (D)$
2		psgnunilem4.t	$⊢ T = ran pmTrsp (D)$
3		psgnunilem4.d	$⊢ φ \to D \in V$
4		psgnunilem4.w1	$⊢ φ \to W \in Word T$
5		psgnunilem4.w2	$⊢ φ \to \sum_{G} W = {I ↾}_{D}$
6		wrdfin	$⊢ W \in Word T \to W \in Fin$
7		hashcl	$⊢ W \in Fin \to \|W\| \in ℕ_{0}$
8	4 6 7	3syl	$⊢ φ \to \|W\| \in ℕ_{0}$
9		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
10	8 9	eleqtrdi	$⊢ φ \to \|W\| \in ℤ_{\geq 0}$
11		fveq2	$⊢ w = \emptyset \to \|w\| = \|\emptyset\|$
12		hash0	$⊢ \|\emptyset\| = 0$
13	11 12	eqtrdi	$⊢ w = \emptyset \to \|w\| = 0$
14	13	oveq2d	$⊢ w = \emptyset \to {(- 1)}^{\|w\|} = {(- 1)}^{0}$
15		neg1cn	$⊢ - 1 \in ℂ$
16		exp0	$⊢ - 1 \in ℂ \to {(- 1)}^{0} = 1$
17	15 16	ax-mp	$⊢ {(- 1)}^{0} = 1$
18	14 17	eqtrdi	$⊢ w = \emptyset \to {(- 1)}^{\|w\|} = 1$
19	18	2a1d	$⊢ w = \emptyset \to ((φ \land \forall x (\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1))) \to ((w \in Word T \land \sum_{G} w = {I ↾}_{D}) \to {(- 1)}^{\|w\|} = 1))$
20		simpl1	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land \neg \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to φ$
21	20 3	syl	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land \neg \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to D \in V$
22		simpl3l	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land \neg \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to w \in Word T$
23		eqidd	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land \neg \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to \|w\| = \|w\|$
24		wrdfin	$⊢ w \in Word T \to w \in Fin$
25	22 24	syl	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land \neg \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to w \in Fin$
26		simpl2	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land \neg \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to w \neq \emptyset$
27		hashnncl	$⊢ w \in Fin \to (\|w\| \in ℕ \leftrightarrow w \neq \emptyset)$
28	27	biimpar	$⊢ (w \in Fin \land w \neq \emptyset) \to \|w\| \in ℕ$
29	25 26 28	syl2anc	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land \neg \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to \|w\| \in ℕ$
30		simpl3r	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land \neg \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to \sum_{G} w = {I ↾}_{D}$
31		fveqeq2	$⊢ x = y \to (\|x\| = \|w\| - 2 \leftrightarrow \|y\| = \|w\| - 2)$
32		oveq2	$⊢ x = y \to \sum_{G} x = \sum_{G} y$
33	32	eqeq1d	$⊢ x = y \to (\sum_{G} x = {I ↾}_{D} \leftrightarrow \sum_{G} y = {I ↾}_{D})$
34	31 33	anbi12d	$⊢ x = y \to ((\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}) \leftrightarrow (\|y\| = \|w\| - 2 \land \sum_{G} y = {I ↾}_{D}))$
35	34	cbvrexvw	$⊢ \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}) \leftrightarrow \exists y \in Word T (\|y\| = \|w\| - 2 \land \sum_{G} y = {I ↾}_{D})$
36	35	notbii	$⊢ \neg \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}) \leftrightarrow \neg \exists y \in Word T (\|y\| = \|w\| - 2 \land \sum_{G} y = {I ↾}_{D})$
37	36	bilani	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land \neg \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to \neg \exists y \in Word T (\|y\| = \|w\| - 2 \land \sum_{G} y = {I ↾}_{D})$
38	1 2 21 22 23 29 30 37	psgnunilem3	$⊢ \neg ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land \neg \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))$
39		iman	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \leftrightarrow \neg ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land \neg \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))$
40	38 39	mpbir	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})$
41		df-rex	$⊢ \exists x \in Word T (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}) \leftrightarrow \exists x (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))$
42	40 41	sylib	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to \exists x (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))$
43		simprl	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to x \in Word T$
44		simprrr	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to \sum_{G} x = {I ↾}_{D}$
45	43 44	jca	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to (x \in Word T \land \sum_{G} x = {I ↾}_{D})$
46		wrdfin	$⊢ x \in Word T \to x \in Fin$
47		hashcl	$⊢ x \in Fin \to \|x\| \in ℕ_{0}$
48	43 46 47	3syl	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to \|x\| \in ℕ_{0}$
49		simp3l	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to w \in Word T$
50	49 24	syl	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to w \in Fin$
51		simp2	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to w \neq \emptyset$
52	50 51 28	syl2anc	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to \|w\| \in ℕ$
53	52	adantr	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to \|w\| \in ℕ$
54		simprrl	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to \|x\| = \|w\| - 2$
55	53	nnred	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to \|w\| \in ℝ$
56		2rp	$⊢ 2 \in ℝ^{+}$
57		ltsubrp	$⊢ (\|w\| \in ℝ \land 2 \in ℝ^{+}) \to \|w\| - 2 < \|w\|$
58	55 56 57	sylancl	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to \|w\| - 2 < \|w\|$
59	54 58	eqbrtrd	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to \|x\| < \|w\|$
60		elfzo0	$⊢ \|x\| \in (0 ..^\|w\|) \leftrightarrow (\|x\| \in ℕ_{0} \land \|w\| \in ℕ \land \|x\| < \|w\|)$
61	48 53 59 60	syl3anbrc	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to \|x\| \in (0 ..^\|w\|)$
62		id	$⊢ (\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1)) \to (\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1))$
63	62	com13	$⊢ (x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to (\|x\| \in (0 ..^\|w\|) \to ((\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1)) \to {(- 1)}^{\|x\|} = 1))$
64	45 61 63	sylc	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to ((\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1)) \to {(- 1)}^{\|x\|} = 1)$
65	54	oveq2d	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to {(- 1)}^{\|x\|} = {(- 1)}^{\|w\| - 2}$
66	15	a1i	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to - 1 \in ℂ$
67		neg1ne0	$⊢ - 1 \neq 0$
68	67	a1i	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to - 1 \neq 0$
69		2z	$⊢ 2 \in ℤ$
70	69	a1i	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to 2 \in ℤ$
71	53	nnzd	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to \|w\| \in ℤ$
72	66 68 70 71	expsubd	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to {(- 1)}^{\|w\| - 2} = \frac{{(- 1)}^{\|w\|}}{{(- 1)}^{2}}$
73		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
74	73	oveq2i	$⊢ \frac{{(- 1)}^{\|w\|}}{{(- 1)}^{2}} = \frac{{(- 1)}^{\|w\|}}{1}$
75		m1expcl	$⊢ \|w\| \in ℤ \to {(- 1)}^{\|w\|} \in ℤ$
76	75	zcnd	$⊢ \|w\| \in ℤ \to {(- 1)}^{\|w\|} \in ℂ$
77	71 76	syl	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to {(- 1)}^{\|w\|} \in ℂ$
78	77	div1d	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to \frac{{(- 1)}^{\|w\|}}{1} = {(- 1)}^{\|w\|}$
79	74 78	eqtrid	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to \frac{{(- 1)}^{\|w\|}}{{(- 1)}^{2}} = {(- 1)}^{\|w\|}$
80	65 72 79	3eqtrd	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to {(- 1)}^{\|x\|} = {(- 1)}^{\|w\|}$
81	80	eqeq1d	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to ({(- 1)}^{\|x\|} = 1 \leftrightarrow {(- 1)}^{\|w\|} = 1)$
82	64 81	sylibd	$⊢ ((φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \land (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D}))) \to ((\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1)) \to {(- 1)}^{\|w\|} = 1)$
83	82	ex	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to ((x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to ((\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1)) \to {(- 1)}^{\|w\|} = 1))$
84	83	com23	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to ((\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1)) \to ((x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to {(- 1)}^{\|w\|} = 1))$
85	84	alimdv	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to (\forall x (\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1)) \to \forall x ((x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to {(- 1)}^{\|w\|} = 1))$
86		19.23v	$⊢ \forall x ((x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to {(- 1)}^{\|w\|} = 1) \leftrightarrow (\exists x (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to {(- 1)}^{\|w\|} = 1)$
87	85 86	imbitrdi	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to (\forall x (\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1)) \to (\exists x (x \in Word T \land (\|x\| = \|w\| - 2 \land \sum_{G} x = {I ↾}_{D})) \to {(- 1)}^{\|w\|} = 1))$
88	42 87	mpid	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to (\forall x (\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1)) \to {(- 1)}^{\|w\|} = 1)$
89	88	3exp	$⊢ φ \to (w \neq \emptyset \to ((w \in Word T \land \sum_{G} w = {I ↾}_{D}) \to (\forall x (\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1)) \to {(- 1)}^{\|w\|} = 1)))$
90	89	com34	$⊢ φ \to (w \neq \emptyset \to (\forall x (\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1)) \to ((w \in Word T \land \sum_{G} w = {I ↾}_{D}) \to {(- 1)}^{\|w\|} = 1)))$
91	90	com12	$⊢ w \neq \emptyset \to (φ \to (\forall x (\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1)) \to ((w \in Word T \land \sum_{G} w = {I ↾}_{D}) \to {(- 1)}^{\|w\|} = 1)))$
92	91	impd	$⊢ w \neq \emptyset \to ((φ \land \forall x (\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1))) \to ((w \in Word T \land \sum_{G} w = {I ↾}_{D}) \to {(- 1)}^{\|w\|} = 1))$
93	19 92	pm2.61ine	$⊢ (φ \land \forall x (\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1))) \to ((w \in Word T \land \sum_{G} w = {I ↾}_{D}) \to {(- 1)}^{\|w\|} = 1)$
94	93	3adant2	$⊢ (φ \land \|w\| \in (0 \dots \|W\|) \land \forall x (\|x\| \in (0 ..^\|w\|) \to ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1))) \to ((w \in Word T \land \sum_{G} w = {I ↾}_{D}) \to {(- 1)}^{\|w\|} = 1)$
95		eleq1	$⊢ w = x \to (w \in Word T \leftrightarrow x \in Word T)$
96		oveq2	$⊢ w = x \to \sum_{G} w = \sum_{G} x$
97	96	eqeq1d	$⊢ w = x \to (\sum_{G} w = {I ↾}_{D} \leftrightarrow \sum_{G} x = {I ↾}_{D})$
98	95 97	anbi12d	$⊢ w = x \to ((w \in Word T \land \sum_{G} w = {I ↾}_{D}) \leftrightarrow (x \in Word T \land \sum_{G} x = {I ↾}_{D}))$
99		fveq2	$⊢ w = x \to \|w\| = \|x\|$
100	99	oveq2d	$⊢ w = x \to {(- 1)}^{\|w\|} = {(- 1)}^{\|x\|}$
101	100	eqeq1d	$⊢ w = x \to ({(- 1)}^{\|w\|} = 1 \leftrightarrow {(- 1)}^{\|x\|} = 1)$
102	98 101	imbi12d	$⊢ w = x \to (((w \in Word T \land \sum_{G} w = {I ↾}_{D}) \to {(- 1)}^{\|w\|} = 1) \leftrightarrow ((x \in Word T \land \sum_{G} x = {I ↾}_{D}) \to {(- 1)}^{\|x\|} = 1))$
103		eleq1	$⊢ w = W \to (w \in Word T \leftrightarrow W \in Word T)$
104		oveq2	$⊢ w = W \to \sum_{G} w = \sum_{G} W$
105	104	eqeq1d	$⊢ w = W \to (\sum_{G} w = {I ↾}_{D} \leftrightarrow \sum_{G} W = {I ↾}_{D})$
106	103 105	anbi12d	$⊢ w = W \to ((w \in Word T \land \sum_{G} w = {I ↾}_{D}) \leftrightarrow (W \in Word T \land \sum_{G} W = {I ↾}_{D}))$
107		fveq2	$⊢ w = W \to \|w\| = \|W\|$
108	107	oveq2d	$⊢ w = W \to {(- 1)}^{\|w\|} = {(- 1)}^{\|W\|}$
109	108	eqeq1d	$⊢ w = W \to ({(- 1)}^{\|w\|} = 1 \leftrightarrow {(- 1)}^{\|W\|} = 1)$
110	106 109	imbi12d	$⊢ w = W \to (((w \in Word T \land \sum_{G} w = {I ↾}_{D}) \to {(- 1)}^{\|w\|} = 1) \leftrightarrow ((W \in Word T \land \sum_{G} W = {I ↾}_{D}) \to {(- 1)}^{\|W\|} = 1))$
111	4 10 94 102 110 99 107	uzindi	$⊢ φ \to ((W \in Word T \land \sum_{G} W = {I ↾}_{D}) \to {(- 1)}^{\|W\|} = 1)$
112	4 5 111	mp2and	$⊢ φ \to {(- 1)}^{\|W\|} = 1$

Metamath Proof Explorer

Theorem psgnunilem4

Proof