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	biimpi	$⊢ \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	37	adantl	$⊢ ((φ \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})$
39	1 2 21 22 23 29 30 38	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}))$
40		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}))$
41	39 40	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})$
42		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}))$
43	41 42	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}))$
44		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$
45		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}$
46	44 45	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})$
47		wrdfin	$⊢ x \in Word T \to x \in Fin$
48		hashcl	$⊢ x \in Fin \to \|x\| \in ℕ_{0}$
49	44 47 48	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}$
50		simp3l	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to w \in Word T$
51	50 24	syl	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to w \in Fin$
52		simp2	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to w \neq \emptyset$
53	51 52 28	syl2anc	$⊢ (φ \land w \neq \emptyset \land (w \in Word T \land \sum_{G} w = {I ↾}_{D})) \to \|w\| \in ℕ$
54	53	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 ℕ$
55		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$
56	54	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 ℝ$
57		2rp	$⊢ 2 \in ℝ^{+}$
58		ltsubrp	$⊢ (\|w\| \in ℝ \land 2 \in ℝ^{+}) \to \|w\| - 2 < \|w\|$
59	56 57 58	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\|$
60	55 59	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\|$
61		elfzo0	$⊢ \|x\| \in (0 ..^\|w\|) \leftrightarrow (\|x\| \in ℕ_{0} \land \|w\| \in ℕ \land \|x\| < \|w\|)$
62	49 54 60 61	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\|)$
63		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))$
64	63	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))$
65	46 62 64	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)$
66	55	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}$
67	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 ℂ$
68		neg1ne0	$⊢ - 1 \neq 0$
69	68	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$
70		2z	$⊢ 2 \in ℤ$
71	70	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 ℤ$
72	54	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 ℤ$
73	67 69 71 72	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}}$
74		neg1sqe1	$⊢ {(- 1)}^{2} = 1$
75	74	oveq2i	$⊢ \frac{{(- 1)}^{\|w\|}}{{(- 1)}^{2}} = \frac{{(- 1)}^{\|w\|}}{1}$
76		m1expcl	$⊢ \|w\| \in ℤ \to {(- 1)}^{\|w\|} \in ℤ$
77	76	zcnd	$⊢ \|w\| \in ℤ \to {(- 1)}^{\|w\|} \in ℂ$
78	72 77	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 ℂ$
79	78	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\|}$
80	75 79	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\|}$
81	66 73 80	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\|}$
82	81	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)$
83	65 82	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)$
84	83	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))$
85	84	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))$
86	85	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))$
87		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)$
88	86 87	syl6ib	$⊢ (φ \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))$
89	43 88	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)$
90	89	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)))$
91	90	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)))$
92	91	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)))$
93	92	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))$
94	19 93	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)$
95	94	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)$
96		eleq1	$⊢ w = x \to (w \in Word T \leftrightarrow x \in Word T)$
97		oveq2	$⊢ w = x \to \sum_{G} w = \sum_{G} x$
98	97	eqeq1d	$⊢ w = x \to (\sum_{G} w = {I ↾}_{D} \leftrightarrow \sum_{G} x = {I ↾}_{D})$
99	96 98	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}))$
100		fveq2	$⊢ w = x \to \|w\| = \|x\|$
101	100	oveq2d	$⊢ w = x \to {(- 1)}^{\|w\|} = {(- 1)}^{\|x\|}$
102	101	eqeq1d	$⊢ w = x \to ({(- 1)}^{\|w\|} = 1 \leftrightarrow {(- 1)}^{\|x\|} = 1)$
103	99 102	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))$
104		eleq1	$⊢ w = W \to (w \in Word T \leftrightarrow W \in Word T)$
105		oveq2	$⊢ w = W \to \sum_{G} w = \sum_{G} W$
106	105	eqeq1d	$⊢ w = W \to (\sum_{G} w = {I ↾}_{D} \leftrightarrow \sum_{G} W = {I ↾}_{D})$
107	104 106	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}))$
108		fveq2	$⊢ w = W \to \|w\| = \|W\|$
109	108	oveq2d	$⊢ w = W \to {(- 1)}^{\|w\|} = {(- 1)}^{\|W\|}$
110	109	eqeq1d	$⊢ w = W \to ({(- 1)}^{\|w\|} = 1 \leftrightarrow {(- 1)}^{\|W\|} = 1)$
111	107 110	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))$
112	4 10 95 103 111 100 108	uzindi	$⊢ φ \to ((W \in Word T \land \sum_{G} W = {I ↾}_{D}) \to {(- 1)}^{\|W\|} = 1)$
113	4 5 112	mp2and	$⊢ φ \to {(- 1)}^{\|W\|} = 1$

Metamath Proof Explorer

Theorem psgnunilem4

Proof