psgnunilem2

Description: Lemma for psgnuni . Induction step for moving a transposition as far to the right as possible. (Contributed by Stefan O'Rear, 24-Aug-2015) (Revised by Mario Carneiro, 28-Feb-2016)

	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)$
	psgnunilem2.in	$⊢ φ \to \neg \exists x \in Word T (\|x\| = L - 2 \land \sum_{G} x = {I ↾}_{D})$
Assertion	psgnunilem2	$⊢ φ \to \exists w \in Word T ((\sum_{G} w = {I ↾}_{D} \land \|w\| = L) \land (I + 1 \in (0 ..^L) \land A \in dom (w (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom (w (j) ∖ I)))$

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		psgnunilem2.in	$⊢ φ \to \neg \exists x \in Word T (\|x\| = L - 2 \land \sum_{G} x = {I ↾}_{D})$
11		wrd0	$⊢ \emptyset \in Word T$
12		splcl	$⊢ (W \in Word T \land \emptyset \in Word T) \to W splice ⟨I, I + 2, \emptyset⟩ \in Word T$
13	4 11 12	sylancl	$⊢ φ \to W splice ⟨I, I + 2, \emptyset⟩ \in Word T$
14	13	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to W splice ⟨I, I + 2, \emptyset⟩ \in Word T$
15		fzossfz	$⊢ (0 ..^L) \subseteq (0 \dots L)$
16	15 7	sselid	$⊢ φ \to I \in (0 \dots L)$
17		elfznn0	$⊢ I \in (0 \dots L) \to I \in ℕ_{0}$
18	16 17	syl	$⊢ φ \to I \in ℕ_{0}$
19		2nn0	$⊢ 2 \in ℕ_{0}$
20		nn0addcl	$⊢ (I \in ℕ_{0} \land 2 \in ℕ_{0}) \to I + 2 \in ℕ_{0}$
21	18 19 20	sylancl	$⊢ φ \to I + 2 \in ℕ_{0}$
22	18	nn0red	$⊢ φ \to I \in ℝ$
23		nn0addge1	$⊢ (I \in ℝ \land 2 \in ℕ_{0}) \to I \leq I + 2$
24	22 19 23	sylancl	$⊢ φ \to I \leq I + 2$
25		elfz2nn0	$⊢ I \in (0 \dots I + 2) \leftrightarrow (I \in ℕ_{0} \land I + 2 \in ℕ_{0} \land I \leq I + 2)$
26	18 21 24 25	syl3anbrc	$⊢ φ \to I \in (0 \dots I + 2)$
27	1 2 3 4 5 6 7 8 9	psgnunilem5	$⊢ φ \to I + 1 \in (0 ..^L)$
28		fzofzp1	$⊢ I + 1 \in (0 ..^L) \to I + 1 + 1 \in (0 \dots L)$
29	27 28	syl	$⊢ φ \to I + 1 + 1 \in (0 \dots L)$
30		df-2	$⊢ 2 = 1 + 1$
31	30	oveq2i	$⊢ I + 2 = I + 1 + 1$
32	18	nn0cnd	$⊢ φ \to I \in ℂ$
33		1cnd	$⊢ φ \to 1 \in ℂ$
34	32 33 33	addassd	$⊢ φ \to I + 1 + 1 = I + 1 + 1$
35	31 34	eqtr4id	$⊢ φ \to I + 2 = I + 1 + 1$
36	6	oveq2d	$⊢ φ \to (0 \dots \|W\|) = (0 \dots L)$
37	29 35 36	3eltr4d	$⊢ φ \to I + 2 \in (0 \dots \|W\|)$
38	11	a1i	$⊢ φ \to \emptyset \in Word T$
39	4 26 37 38	spllen	$⊢ φ \to \|W splice ⟨I, I + 2, \emptyset⟩\| = \|W\| + \|\emptyset\| - (I + 2 - I)$
40		hash0	$⊢ \|\emptyset\| = 0$
41	40	oveq1i	$⊢ \|\emptyset\| - (I + 2 - I) = 0 - (I + 2 - I)$
42		df-neg	$⊢ - (I + 2 - I) = 0 - (I + 2 - I)$
43	41 42	eqtr4i	$⊢ \|\emptyset\| - (I + 2 - I) = - (I + 2 - I)$
44		2cn	$⊢ 2 \in ℂ$
45		pncan2	$⊢ (I \in ℂ \land 2 \in ℂ) \to I + 2 - I = 2$
46	32 44 45	sylancl	$⊢ φ \to I + 2 - I = 2$
47	46	negeqd	$⊢ φ \to - (I + 2 - I) = - 2$
48	43 47	eqtrid	$⊢ φ \to \|\emptyset\| - (I + 2 - I) = - 2$
49	6 48	oveq12d	$⊢ φ \to \|W\| + \|\emptyset\| - (I + 2 - I) = L + -2$
50		elfzel2	$⊢ I \in (0 \dots L) \to L \in ℤ$
51	16 50	syl	$⊢ φ \to L \in ℤ$
52	51	zcnd	$⊢ φ \to L \in ℂ$
53		negsub	$⊢ (L \in ℂ \land 2 \in ℂ) \to L + -2 = L - 2$
54	52 44 53	sylancl	$⊢ φ \to L + -2 = L - 2$
55	39 49 54	3eqtrd	$⊢ φ \to \|W splice ⟨I, I + 2, \emptyset⟩\| = L - 2$
56	55	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \|W splice ⟨I, I + 2, \emptyset⟩\| = L - 2$
57		splid	$⊢ (W \in Word T \land (I \in (0 \dots I + 2) \land I + 2 \in (0 \dots \|W\|))) \to W splice ⟨I, I + 2, W substr ⟨I, I + 2⟩⟩ = W$
58	4 26 37 57	syl12anc	$⊢ φ \to W splice ⟨I, I + 2, W substr ⟨I, I + 2⟩⟩ = W$
59	58	oveq2d	$⊢ φ \to \sum_{G} (W splice ⟨I, I + 2, W substr ⟨I, I + 2⟩⟩) = \sum_{G} W$
60	59	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \sum_{G} (W splice ⟨I, I + 2, W substr ⟨I, I + 2⟩⟩) = \sum_{G} W$
61		eqid	$⊢ {Base}_{G} = {Base}_{G}$
62	1	symggrp	$⊢ D \in V \to G \in Grp$
63	3 62	syl	$⊢ φ \to G \in Grp$
64	63	grpmndd	$⊢ φ \to G \in Mnd$
65	64	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to G \in Mnd$
66	2 1 61	symgtrf	$⊢ T \subseteq {Base}_{G}$
67		sswrd	$⊢ T \subseteq {Base}_{G} \to Word T \subseteq Word {Base}_{G}$
68	66 67	ax-mp	$⊢ Word T \subseteq Word {Base}_{G}$
69	68 4	sselid	$⊢ φ \to W \in Word {Base}_{G}$
70	69	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to W \in Word {Base}_{G}$
71	26	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to I \in (0 \dots I + 2)$
72	37	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to I + 2 \in (0 \dots \|W\|)$
73		swrdcl	$⊢ W \in Word {Base}_{G} \to W substr ⟨I, I + 2⟩ \in Word {Base}_{G}$
74	69 73	syl	$⊢ φ \to W substr ⟨I, I + 2⟩ \in Word {Base}_{G}$
75	74	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to W substr ⟨I, I + 2⟩ \in Word {Base}_{G}$
76		wrd0	$⊢ \emptyset \in Word {Base}_{G}$
77	76	a1i	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \emptyset \in Word {Base}_{G}$
78	6	oveq2d	$⊢ φ \to (0 ..^\|W\|) = (0 ..^L)$
79	27 78	eleqtrrd	$⊢ φ \to I + 1 \in (0 ..^\|W\|)$
80		swrds2	$⊢ (W \in Word T \land I \in ℕ_{0} \land I + 1 \in (0 ..^\|W\|)) \to W substr ⟨I, I + 2⟩ = ⟨“ W (I) W (I + 1) ”⟩$
81	4 18 79 80	syl3anc	$⊢ φ \to W substr ⟨I, I + 2⟩ = ⟨“ W (I) W (I + 1) ”⟩$
82	81	oveq2d	$⊢ φ \to \sum_{G} (W substr ⟨I, I + 2⟩) = \sum_{G} ⟨“ W (I) W (I + 1) ”⟩$
83		wrdf	$⊢ W \in Word T \to W : (0 ..^\|W\|) ⟶ T$
84	4 83	syl	$⊢ φ \to W : (0 ..^\|W\|) ⟶ T$
85	78	feq2d	$⊢ φ \to (W : (0 ..^\|W\|) ⟶ T \leftrightarrow W : (0 ..^L) ⟶ T)$
86	84 85	mpbid	$⊢ φ \to W : (0 ..^L) ⟶ T$
87	86 7	ffvelcdmd	$⊢ φ \to W (I) \in T$
88	66 87	sselid	$⊢ φ \to W (I) \in {Base}_{G}$
89	86 27	ffvelcdmd	$⊢ φ \to W (I + 1) \in T$
90	66 89	sselid	$⊢ φ \to W (I + 1) \in {Base}_{G}$
91		eqid	$⊢ +_{G} = +_{G}$
92	61 91	gsumws2	$⊢ (G \in Mnd \land W (I) \in {Base}_{G} \land W (I + 1) \in {Base}_{G}) \to \sum_{G} ⟨“ W (I) W (I + 1) ”⟩ = W (I) +_{G} W (I + 1)$
93	64 88 90 92	syl3anc	$⊢ φ \to \sum_{G} ⟨“ W (I) W (I + 1) ”⟩ = W (I) +_{G} W (I + 1)$
94	1 61 91	symgov	$⊢ (W (I) \in {Base}_{G} \land W (I + 1) \in {Base}_{G}) \to W (I) +_{G} W (I + 1) = W (I) \circ W (I + 1)$
95	88 90 94	syl2anc	$⊢ φ \to W (I) +_{G} W (I + 1) = W (I) \circ W (I + 1)$
96	82 93 95	3eqtrd	$⊢ φ \to \sum_{G} (W substr ⟨I, I + 2⟩) = W (I) \circ W (I + 1)$
97	96	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \sum_{G} (W substr ⟨I, I + 2⟩) = W (I) \circ W (I + 1)$
98		simpr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to W (I) \circ W (I + 1) = {I ↾}_{D}$
99	1	symgid	$⊢ D \in V \to {I ↾}_{D} = 0_{G}$
100	3 99	syl	$⊢ φ \to {I ↾}_{D} = 0_{G}$
101		eqid	$⊢ 0_{G} = 0_{G}$
102	101	gsum0	$⊢ \sum_{G} \emptyset = 0_{G}$
103	100 102	eqtr4di	$⊢ φ \to {I ↾}_{D} = \sum_{G} \emptyset$
104	103	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to {I ↾}_{D} = \sum_{G} \emptyset$
105	97 98 104	3eqtrd	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \sum_{G} (W substr ⟨I, I + 2⟩) = \sum_{G} \emptyset$
106	61 65 70 71 72 75 77 105	gsumspl	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \sum_{G} (W splice ⟨I, I + 2, W substr ⟨I, I + 2⟩⟩) = \sum_{G} (W splice ⟨I, I + 2, \emptyset⟩)$
107	5	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \sum_{G} W = {I ↾}_{D}$
108	60 106 107	3eqtr3d	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \sum_{G} (W splice ⟨I, I + 2, \emptyset⟩) = {I ↾}_{D}$
109		fveqeq2	$⊢ x = W splice ⟨I, I + 2, \emptyset⟩ \to (\|x\| = L - 2 \leftrightarrow \|W splice ⟨I, I + 2, \emptyset⟩\| = L - 2)$
110		oveq2	$⊢ x = W splice ⟨I, I + 2, \emptyset⟩ \to \sum_{G} x = \sum_{G} (W splice ⟨I, I + 2, \emptyset⟩)$
111	110	eqeq1d	$⊢ x = W splice ⟨I, I + 2, \emptyset⟩ \to (\sum_{G} x = {I ↾}_{D} \leftrightarrow \sum_{G} (W splice ⟨I, I + 2, \emptyset⟩) = {I ↾}_{D})$
112	109 111	anbi12d	$⊢ x = W splice ⟨I, I + 2, \emptyset⟩ \to ((\|x\| = L - 2 \land \sum_{G} x = {I ↾}_{D}) \leftrightarrow (\|W splice ⟨I, I + 2, \emptyset⟩\| = L - 2 \land \sum_{G} (W splice ⟨I, I + 2, \emptyset⟩) = {I ↾}_{D}))$
113	112	rspcev	$⊢ (W splice ⟨I, I + 2, \emptyset⟩ \in Word T \land (\|W splice ⟨I, I + 2, \emptyset⟩\| = L - 2 \land \sum_{G} (W splice ⟨I, I + 2, \emptyset⟩) = {I ↾}_{D})) \to \exists x \in Word T (\|x\| = L - 2 \land \sum_{G} x = {I ↾}_{D})$
114	14 56 108 113	syl12anc	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \exists x \in Word T (\|x\| = L - 2 \land \sum_{G} x = {I ↾}_{D})$
115	10	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \neg \exists x \in Word T (\|x\| = L - 2 \land \sum_{G} x = {I ↾}_{D})$
116	114 115	pm2.21dd	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \exists w \in Word T ((\sum_{G} w = {I ↾}_{D} \land \|w\| = L) \land (I + 1 \in (0 ..^L) \land A \in dom (w (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom (w (j) ∖ I)))$
117	116	ex	$⊢ φ \to (W (I) \circ W (I + 1) = {I ↾}_{D} \to \exists w \in Word T ((\sum_{G} w = {I ↾}_{D} \land \|w\| = L) \land (I + 1 \in (0 ..^L) \land A \in dom (w (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom (w (j) ∖ I))))$
118	4	adantr	$⊢ (φ \land (r \in T \land s \in T)) \to W \in Word T$
119		simprl	$⊢ (φ \land (r \in T \land s \in T)) \to r \in T$
120		simprr	$⊢ (φ \land (r \in T \land s \in T)) \to s \in T$
121	119 120	s2cld	$⊢ (φ \land (r \in T \land s \in T)) \to ⟨“ r s ”⟩ \in Word T$
122		splcl	$⊢ (W \in Word T \land ⟨“ r s ”⟩ \in Word T) \to W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \in Word T$
123	118 121 122	syl2anc	$⊢ (φ \land (r \in T \land s \in T)) \to W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \in Word T$
124	123	adantrr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \in Word T$
125	64	adantr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to G \in Mnd$
126	69	adantr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to W \in Word {Base}_{G}$
127	26	adantr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to I \in (0 \dots I + 2)$
128	37	adantr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to I + 2 \in (0 \dots \|W\|)$
129	68 121	sselid	$⊢ (φ \land (r \in T \land s \in T)) \to ⟨“ r s ”⟩ \in Word {Base}_{G}$
130	129	adantrr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to ⟨“ r s ”⟩ \in Word {Base}_{G}$
131	74	adantr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to W substr ⟨I, I + 2⟩ \in Word {Base}_{G}$
132		simprr1	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to W (I) \circ W (I + 1) = r \circ s$
133	96	adantr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to \sum_{G} (W substr ⟨I, I + 2⟩) = W (I) \circ W (I + 1)$
134	64	adantr	$⊢ (φ \land (r \in T \land s \in T)) \to G \in Mnd$
135	66	a1i	$⊢ φ \to T \subseteq {Base}_{G}$
136	135	sselda	$⊢ (φ \land r \in T) \to r \in {Base}_{G}$
137	136	adantrr	$⊢ (φ \land (r \in T \land s \in T)) \to r \in {Base}_{G}$
138	135	sselda	$⊢ (φ \land s \in T) \to s \in {Base}_{G}$
139	138	adantrl	$⊢ (φ \land (r \in T \land s \in T)) \to s \in {Base}_{G}$
140	61 91	gsumws2	$⊢ (G \in Mnd \land r \in {Base}_{G} \land s \in {Base}_{G}) \to \sum_{G} ⟨“ r s ”⟩ = r +_{G} s$
141	134 137 139 140	syl3anc	$⊢ (φ \land (r \in T \land s \in T)) \to \sum_{G} ⟨“ r s ”⟩ = r +_{G} s$
142	1 61 91	symgov	$⊢ (r \in {Base}_{G} \land s \in {Base}_{G}) \to r +_{G} s = r \circ s$
143	137 139 142	syl2anc	$⊢ (φ \land (r \in T \land s \in T)) \to r +_{G} s = r \circ s$
144	141 143	eqtrd	$⊢ (φ \land (r \in T \land s \in T)) \to \sum_{G} ⟨“ r s ”⟩ = r \circ s$
145	144	adantrr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to \sum_{G} ⟨“ r s ”⟩ = r \circ s$
146	132 133 145	3eqtr4rd	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to \sum_{G} ⟨“ r s ”⟩ = \sum_{G} (W substr ⟨I, I + 2⟩)$
147	61 125 126 127 128 130 131 146	gsumspl	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to \sum_{G} (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) = \sum_{G} (W splice ⟨I, I + 2, W substr ⟨I, I + 2⟩⟩)$
148	59	adantr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to \sum_{G} (W splice ⟨I, I + 2, W substr ⟨I, I + 2⟩⟩) = \sum_{G} W$
149	5	adantr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to \sum_{G} W = {I ↾}_{D}$
150	147 148 149	3eqtrd	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to \sum_{G} (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) = {I ↾}_{D}$
151	26	adantr	$⊢ (φ \land (r \in T \land s \in T)) \to I \in (0 \dots I + 2)$
152	37	adantr	$⊢ (φ \land (r \in T \land s \in T)) \to I + 2 \in (0 \dots \|W\|)$
153	118 151 152 121	spllen	$⊢ (φ \land (r \in T \land s \in T)) \to \|W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩\| = \|W\| + \|⟨“ r s ”⟩\| - (I + 2 - I)$
154		s2len	$⊢ \|⟨“ r s ”⟩\| = 2$
155	154	oveq1i	$⊢ \|⟨“ r s ”⟩\| - (I + 2 - I) = 2 - (I + 2 - I)$
156	46	oveq2d	$⊢ φ \to 2 - (I + 2 - I) = 2 - 2$
157	44	subidi	$⊢ 2 - 2 = 0$
158	156 157	eqtrdi	$⊢ φ \to 2 - (I + 2 - I) = 0$
159	155 158	eqtrid	$⊢ φ \to \|⟨“ r s ”⟩\| - (I + 2 - I) = 0$
160	159	oveq2d	$⊢ φ \to \|W\| + \|⟨“ r s ”⟩\| - (I + 2 - I) = \|W\| + 0$
161	6 52	eqeltrd	$⊢ φ \to \|W\| \in ℂ$
162	161	addridd	$⊢ φ \to \|W\| + 0 = \|W\|$
163	160 162 6	3eqtrd	$⊢ φ \to \|W\| + \|⟨“ r s ”⟩\| - (I + 2 - I) = L$
164	163	adantr	$⊢ (φ \land (r \in T \land s \in T)) \to \|W\| + \|⟨“ r s ”⟩\| - (I + 2 - I) = L$
165	153 164	eqtrd	$⊢ (φ \land (r \in T \land s \in T)) \to \|W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩\| = L$
166	165	adantrr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to \|W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩\| = L$
167	150 166	jca	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to (\sum_{G} (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) = {I ↾}_{D} \land \|W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩\| = L)$
168	27	adantr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to I + 1 \in (0 ..^L)$
169		simprr2	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to A \in dom (s ∖ I)$
170		1nn0	$⊢ 1 \in ℕ_{0}$
171		2nn	$⊢ 2 \in ℕ$
172		1lt2	$⊢ 1 < 2$
173		elfzo0	$⊢ 1 \in (0 ..^2) \leftrightarrow (1 \in ℕ_{0} \land 2 \in ℕ \land 1 < 2)$
174	170 171 172 173	mpbir3an	$⊢ 1 \in (0 ..^2)$
175	154	oveq2i	$⊢ (0 ..^\|⟨“ r s ”⟩\|) = (0 ..^2)$
176	174 175	eleqtrri	$⊢ 1 \in (0 ..^\|⟨“ r s ”⟩\|)$
177	176	a1i	$⊢ (φ \land (r \in T \land s \in T)) \to 1 \in (0 ..^\|⟨“ r s ”⟩\|)$
178	118 151 152 121 177	splfv2a	$⊢ (φ \land (r \in T \land s \in T)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) = ⟨“ r s ”⟩ (1)$
179		s2fv1	$⊢ s \in T \to ⟨“ r s ”⟩ (1) = s$
180	179	ad2antll	$⊢ (φ \land (r \in T \land s \in T)) \to ⟨“ r s ”⟩ (1) = s$
181	178 180	eqtrd	$⊢ (φ \land (r \in T \land s \in T)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) = s$
182	181	adantrr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) = s$
183	182	difeq1d	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) ∖ I = s ∖ I$
184	183	dmeqd	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) ∖ I) = dom (s ∖ I)$
185	169 184	eleqtrrd	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) ∖ I)$
186		fzosplitsni	$⊢ I \in ℤ_{\geq 0} \to (j \in (0 ..^I + 1) \leftrightarrow (j \in (0 ..^I) \lor j = I))$
187		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
188	186 187	eleq2s	$⊢ I \in ℕ_{0} \to (j \in (0 ..^I + 1) \leftrightarrow (j \in (0 ..^I) \lor j = I))$
189	18 188	syl	$⊢ φ \to (j \in (0 ..^I + 1) \leftrightarrow (j \in (0 ..^I) \lor j = I))$
190	189	adantr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to (j \in (0 ..^I + 1) \leftrightarrow (j \in (0 ..^I) \lor j = I))$
191		fveq2	$⊢ k = j \to W (k) = W (j)$
192	191	difeq1d	$⊢ k = j \to W (k) ∖ I = W (j) ∖ I$
193	192	dmeqd	$⊢ k = j \to dom (W (k) ∖ I) = dom (W (j) ∖ I)$
194	193	eleq2d	$⊢ k = j \to (A \in dom (W (k) ∖ I) \leftrightarrow A \in dom (W (j) ∖ I))$
195	194	notbid	$⊢ k = j \to (\neg A \in dom (W (k) ∖ I) \leftrightarrow \neg A \in dom (W (j) ∖ I))$
196	195	rspccva	$⊢ (\forall k \in (0 ..^I) \neg A \in dom (W (k) ∖ I) \land j \in (0 ..^I)) \to \neg A \in dom (W (j) ∖ I)$
197	9 196	sylan	$⊢ (φ \land j \in (0 ..^I)) \to \neg A \in dom (W (j) ∖ I)$
198	197	adantlr	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to \neg A \in dom (W (j) ∖ I)$
199	4	ad2antrr	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to W \in Word T$
200	26	ad2antrr	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to I \in (0 \dots I + 2)$
201	37	ad2antrr	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to I + 2 \in (0 \dots \|W\|)$
202	121	adantr	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to ⟨“ r s ”⟩ \in Word T$
203		simpr	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to j \in (0 ..^I)$
204	199 200 201 202 203	splfv1	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) = W (j)$
205	204	difeq1d	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I = W (j) ∖ I$
206	205	dmeqd	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I) = dom (W (j) ∖ I)$
207	198 206	neleqtrrd	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I)$
208	207	ex	$⊢ (φ \land (r \in T \land s \in T)) \to (j \in (0 ..^I) \to \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I))$
209	208	adantrr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to (j \in (0 ..^I) \to \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I))$
210		simprr3	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to \neg A \in dom (r ∖ I)$
211		0nn0	$⊢ 0 \in ℕ_{0}$
212		2pos	$⊢ 0 < 2$
213		elfzo0	$⊢ 0 \in (0 ..^2) \leftrightarrow (0 \in ℕ_{0} \land 2 \in ℕ \land 0 < 2)$
214	211 171 212 213	mpbir3an	$⊢ 0 \in (0 ..^2)$
215	214 175	eleqtrri	$⊢ 0 \in (0 ..^\|⟨“ r s ”⟩\|)$
216	215	a1i	$⊢ (φ \land (r \in T \land s \in T)) \to 0 \in (0 ..^\|⟨“ r s ”⟩\|)$
217	118 151 152 121 216	splfv2a	$⊢ (φ \land (r \in T \land s \in T)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 0) = ⟨“ r s ”⟩ (0)$
218	32	addridd	$⊢ φ \to I + 0 = I$
219	218	adantr	$⊢ (φ \land (r \in T \land s \in T)) \to I + 0 = I$
220	219	fveq2d	$⊢ (φ \land (r \in T \land s \in T)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 0) = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I)$
221		s2fv0	$⊢ r \in T \to ⟨“ r s ”⟩ (0) = r$
222	221	ad2antrl	$⊢ (φ \land (r \in T \land s \in T)) \to ⟨“ r s ”⟩ (0) = r$
223	217 220 222	3eqtr3d	$⊢ (φ \land (r \in T \land s \in T)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) = r$
224	223	difeq1d	$⊢ (φ \land (r \in T \land s \in T)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I = r ∖ I$
225	224	dmeqd	$⊢ (φ \land (r \in T \land s \in T)) \to dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I) = dom (r ∖ I)$
226	225	eleq2d	$⊢ (φ \land (r \in T \land s \in T)) \to (A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I) \leftrightarrow A \in dom (r ∖ I))$
227	226	adantrr	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to (A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I) \leftrightarrow A \in dom (r ∖ I))$
228	210 227	mtbird	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I)$
229		fveq2	$⊢ j = I \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I)$
230	229	difeq1d	$⊢ j = I \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I$
231	230	dmeqd	$⊢ j = I \to dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I) = dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I)$
232	231	eleq2d	$⊢ j = I \to (A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I) \leftrightarrow A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I))$
233	232	notbid	$⊢ j = I \to (\neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I) \leftrightarrow \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I))$
234	228 233	syl5ibrcom	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to (j = I \to \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I))$
235	209 234	jaod	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to ((j \in (0 ..^I) \lor j = I) \to \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I))$
236	190 235	sylbid	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to (j \in (0 ..^I + 1) \to \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I))$
237	236	ralrimiv	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to \forall j \in (0 ..^I + 1) \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I)$
238	168 185 237	3jca	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to (I + 1 \in (0 ..^L) \land A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I))$
239		oveq2	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to \sum_{G} w = \sum_{G} (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩)$
240	239	eqeq1d	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to (\sum_{G} w = {I ↾}_{D} \leftrightarrow \sum_{G} (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) = {I ↾}_{D})$
241		fveqeq2	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to (\|w\| = L \leftrightarrow \|W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩\| = L)$
242	240 241	anbi12d	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to ((\sum_{G} w = {I ↾}_{D} \land \|w\| = L) \leftrightarrow (\sum_{G} (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) = {I ↾}_{D} \land \|W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩\| = L))$
243		fveq1	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to w (I + 1) = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1)$
244	243	difeq1d	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to w (I + 1) ∖ I = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) ∖ I$
245	244	dmeqd	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to dom (w (I + 1) ∖ I) = dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) ∖ I)$
246	245	eleq2d	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to (A \in dom (w (I + 1) ∖ I) \leftrightarrow A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) ∖ I))$
247		fveq1	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to w (j) = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j)$
248	247	difeq1d	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to w (j) ∖ I = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I$
249	248	dmeqd	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to dom (w (j) ∖ I) = dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I)$
250	249	eleq2d	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to (A \in dom (w (j) ∖ I) \leftrightarrow A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I))$
251	250	notbid	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to (\neg A \in dom (w (j) ∖ I) \leftrightarrow \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I))$
252	251	ralbidv	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to (\forall j \in (0 ..^I + 1) \neg A \in dom (w (j) ∖ I) \leftrightarrow \forall j \in (0 ..^I + 1) \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I))$
253	246 252	3anbi23d	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to ((I + 1 \in (0 ..^L) \land A \in dom (w (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom (w (j) ∖ I)) \leftrightarrow (I + 1 \in (0 ..^L) \land A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I)))$
254	242 253	anbi12d	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to (((\sum_{G} w = {I ↾}_{D} \land \|w\| = L) \land (I + 1 \in (0 ..^L) \land A \in dom (w (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom (w (j) ∖ I))) \leftrightarrow ((\sum_{G} (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) = {I ↾}_{D} \land \|W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩\| = L) \land (I + 1 \in (0 ..^L) \land A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I))))$
255	254	rspcev	$⊢ (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \in Word T \land ((\sum_{G} (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) = {I ↾}_{D} \land \|W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩\| = L) \land (I + 1 \in (0 ..^L) \land A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I)))) \to \exists w \in Word T ((\sum_{G} w = {I ↾}_{D} \land \|w\| = L) \land (I + 1 \in (0 ..^L) \land A \in dom (w (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom (w (j) ∖ I)))$
256	124 167 238 255	syl12anc	$⊢ (φ \land ((r \in T \land s \in T) \land (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))) \to \exists w \in Word T ((\sum_{G} w = {I ↾}_{D} \land \|w\| = L) \land (I + 1 \in (0 ..^L) \land A \in dom (w (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom (w (j) ∖ I)))$
257	256	expr	$⊢ (φ \land (r \in T \land s \in T)) \to ((W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)) \to \exists w \in Word T ((\sum_{G} w = {I ↾}_{D} \land \|w\| = L) \land (I + 1 \in (0 ..^L) \land A \in dom (w (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom (w (j) ∖ I))))$
258	257	rexlimdvva	$⊢ φ \to (\exists r \in T \exists s \in T (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)) \to \exists w \in Word T ((\sum_{G} w = {I ↾}_{D} \land \|w\| = L) \land (I + 1 \in (0 ..^L) \land A \in dom (w (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom (w (j) ∖ I))))$
259	2 3 87 89 8	psgnunilem1	$⊢ φ \to (W (I) \circ W (I + 1) = {I ↾}_{D} \lor \exists r \in T \exists s \in T (W (I) \circ W (I + 1) = r \circ s \land A \in dom (s ∖ I) \land \neg A \in dom (r ∖ I)))$
260	117 258 259	mpjaod	$⊢ φ \to \exists w \in Word T ((\sum_{G} w = {I ↾}_{D} \land \|w\| = L) \land (I + 1 \in (0 ..^L) \land A \in dom (w (I + 1) ∖ I) \land \forall j \in (0 ..^I + 1) \neg A \in dom (w (j) ∖ I)))$

Metamath Proof Explorer

Theorem psgnunilem2

Proof