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	sseldi	$⊢ φ \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	syl5eq	$⊢ φ \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		grpmnd	$⊢ G \in Grp \to G \in Mnd$
65	63 64	syl	$⊢ φ \to G \in Mnd$
66	65	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to G \in Mnd$
67	2 1 61	symgtrf	$⊢ T \subseteq {Base}_{G}$
68		sswrd	$⊢ T \subseteq {Base}_{G} \to Word T \subseteq Word {Base}_{G}$
69	67 68	ax-mp	$⊢ Word T \subseteq Word {Base}_{G}$
70	69 4	sseldi	$⊢ φ \to W \in Word {Base}_{G}$
71	70	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to W \in Word {Base}_{G}$
72	26	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to I \in (0 \dots I + 2)$
73	37	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to I + 2 \in (0 \dots \|W\|)$
74		swrdcl	$⊢ W \in Word {Base}_{G} \to W substr ⟨I, I + 2⟩ \in Word {Base}_{G}$
75	70 74	syl	$⊢ φ \to W substr ⟨I, I + 2⟩ \in Word {Base}_{G}$
76	75	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to W substr ⟨I, I + 2⟩ \in Word {Base}_{G}$
77		wrd0	$⊢ \emptyset \in Word {Base}_{G}$
78	77	a1i	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \emptyset \in Word {Base}_{G}$
79	6	oveq2d	$⊢ φ \to (0 ..^\|W\|) = (0 ..^L)$
80	27 79	eleqtrrd	$⊢ φ \to I + 1 \in (0 ..^\|W\|)$
81		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) ”⟩$
82	4 18 80 81	syl3anc	$⊢ φ \to W substr ⟨I, I + 2⟩ = ⟨“ W (I) W (I + 1) ”⟩$
83	82	oveq2d	$⊢ φ \to \sum_{G} (W substr ⟨I, I + 2⟩) = \sum_{G} ⟨“ W (I) W (I + 1) ”⟩$
84		wrdf	$⊢ W \in Word T \to W : (0 ..^\|W\|) ⟶ T$
85	4 84	syl	$⊢ φ \to W : (0 ..^\|W\|) ⟶ T$
86	79	feq2d	$⊢ φ \to (W : (0 ..^\|W\|) ⟶ T \leftrightarrow W : (0 ..^L) ⟶ T)$
87	85 86	mpbid	$⊢ φ \to W : (0 ..^L) ⟶ T$
88	87 7	ffvelrnd	$⊢ φ \to W (I) \in T$
89	67 88	sseldi	$⊢ φ \to W (I) \in {Base}_{G}$
90	87 27	ffvelrnd	$⊢ φ \to W (I + 1) \in T$
91	67 90	sseldi	$⊢ φ \to W (I + 1) \in {Base}_{G}$
92		eqid	$⊢ +_{G} = +_{G}$
93	61 92	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)$
94	65 89 91 93	syl3anc	$⊢ φ \to \sum_{G} ⟨“ W (I) W (I + 1) ”⟩ = W (I) +_{G} W (I + 1)$
95	1 61 92	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)$
96	89 91 95	syl2anc	$⊢ φ \to W (I) +_{G} W (I + 1) = W (I) \circ W (I + 1)$
97	83 94 96	3eqtrd	$⊢ φ \to \sum_{G} (W substr ⟨I, I + 2⟩) = W (I) \circ W (I + 1)$
98	97	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \sum_{G} (W substr ⟨I, I + 2⟩) = W (I) \circ W (I + 1)$
99		simpr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to W (I) \circ W (I + 1) = {I ↾}_{D}$
100	1	symgid	$⊢ D \in V \to {I ↾}_{D} = 0_{G}$
101	3 100	syl	$⊢ φ \to {I ↾}_{D} = 0_{G}$
102		eqid	$⊢ 0_{G} = 0_{G}$
103	102	gsum0	$⊢ \sum_{G} \emptyset = 0_{G}$
104	101 103	eqtr4di	$⊢ φ \to {I ↾}_{D} = \sum_{G} \emptyset$
105	104	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to {I ↾}_{D} = \sum_{G} \emptyset$
106	98 99 105	3eqtrd	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \sum_{G} (W substr ⟨I, I + 2⟩) = \sum_{G} \emptyset$
107	61 66 71 72 73 76 78 106	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⟩)$
108	5	adantr	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \sum_{G} W = {I ↾}_{D}$
109	60 107 108	3eqtr3d	$⊢ (φ \land W (I) \circ W (I + 1) = {I ↾}_{D}) \to \sum_{G} (W splice ⟨I, I + 2, \emptyset⟩) = {I ↾}_{D}$
110		fveqeq2	$⊢ x = W splice ⟨I, I + 2, \emptyset⟩ \to (\|x\| = L - 2 \leftrightarrow \|W splice ⟨I, I + 2, \emptyset⟩\| = L - 2)$
111		oveq2	$⊢ x = W splice ⟨I, I + 2, \emptyset⟩ \to \sum_{G} x = \sum_{G} (W splice ⟨I, I + 2, \emptyset⟩)$
112	111	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})$
113	110 112	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}))$
114	113	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})$
115	14 56 109 114	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})$
116	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})$
117	115 116	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)))$
118	117	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))))$
119	4	adantr	$⊢ (φ \land (r \in T \land s \in T)) \to W \in Word T$
120		simprl	$⊢ (φ \land (r \in T \land s \in T)) \to r \in T$
121		simprr	$⊢ (φ \land (r \in T \land s \in T)) \to s \in T$
122	120 121	s2cld	$⊢ (φ \land (r \in T \land s \in T)) \to ⟨“ r s ”⟩ \in Word T$
123		splcl	$⊢ (W \in Word T \land ⟨“ r s ”⟩ \in Word T) \to W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \in Word T$
124	119 122 123	syl2anc	$⊢ (φ \land (r \in T \land s \in T)) \to W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \in Word T$
125	124	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$
126	65	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$
127	70	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}$
128	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)$
129	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\|)$
130	69 122	sseldi	$⊢ (φ \land (r \in T \land s \in T)) \to ⟨“ r s ”⟩ \in Word {Base}_{G}$
131	130	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}$
132	75	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}$
133		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$
134	97	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)$
135	65	adantr	$⊢ (φ \land (r \in T \land s \in T)) \to G \in Mnd$
136	67	a1i	$⊢ φ \to T \subseteq {Base}_{G}$
137	136	sselda	$⊢ (φ \land r \in T) \to r \in {Base}_{G}$
138	137	adantrr	$⊢ (φ \land (r \in T \land s \in T)) \to r \in {Base}_{G}$
139	136	sselda	$⊢ (φ \land s \in T) \to s \in {Base}_{G}$
140	139	adantrl	$⊢ (φ \land (r \in T \land s \in T)) \to s \in {Base}_{G}$
141	61 92	gsumws2	$⊢ (G \in Mnd \land r \in {Base}_{G} \land s \in {Base}_{G}) \to \sum_{G} ⟨“ r s ”⟩ = r +_{G} s$
142	135 138 140 141	syl3anc	$⊢ (φ \land (r \in T \land s \in T)) \to \sum_{G} ⟨“ r s ”⟩ = r +_{G} s$
143	1 61 92	symgov	$⊢ (r \in {Base}_{G} \land s \in {Base}_{G}) \to r +_{G} s = r \circ s$
144	138 140 143	syl2anc	$⊢ (φ \land (r \in T \land s \in T)) \to r +_{G} s = r \circ s$
145	142 144	eqtrd	$⊢ (φ \land (r \in T \land s \in T)) \to \sum_{G} ⟨“ r s ”⟩ = r \circ s$
146	145	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$
147	133 134 146	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⟩)$
148	61 126 127 128 129 131 132 147	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⟩⟩)$
149	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$
150	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}$
151	148 149 150	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}$
152	26	adantr	$⊢ (φ \land (r \in T \land s \in T)) \to I \in (0 \dots I + 2)$
153	37	adantr	$⊢ (φ \land (r \in T \land s \in T)) \to I + 2 \in (0 \dots \|W\|)$
154	119 152 153 122	spllen	$⊢ (φ \land (r \in T \land s \in T)) \to \|W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩\| = \|W\| + \|⟨“ r s ”⟩\| - (I + 2 - I)$
155		s2len	$⊢ \|⟨“ r s ”⟩\| = 2$
156	155	oveq1i	$⊢ \|⟨“ r s ”⟩\| - (I + 2 - I) = 2 - (I + 2 - I)$
157	46	oveq2d	$⊢ φ \to 2 - (I + 2 - I) = 2 - 2$
158	44	subidi	$⊢ 2 - 2 = 0$
159	157 158	eqtrdi	$⊢ φ \to 2 - (I + 2 - I) = 0$
160	156 159	syl5eq	$⊢ φ \to \|⟨“ r s ”⟩\| - (I + 2 - I) = 0$
161	160	oveq2d	$⊢ φ \to \|W\| + \|⟨“ r s ”⟩\| - (I + 2 - I) = \|W\| + 0$
162	6 52	eqeltrd	$⊢ φ \to \|W\| \in ℂ$
163	162	addid1d	$⊢ φ \to \|W\| + 0 = \|W\|$
164	161 163 6	3eqtrd	$⊢ φ \to \|W\| + \|⟨“ r s ”⟩\| - (I + 2 - I) = L$
165	164	adantr	$⊢ (φ \land (r \in T \land s \in T)) \to \|W\| + \|⟨“ r s ”⟩\| - (I + 2 - I) = L$
166	154 165	eqtrd	$⊢ (φ \land (r \in T \land s \in T)) \to \|W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩\| = L$
167	166	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$
168	151 167	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)$
169	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)$
170		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)$
171		1nn0	$⊢ 1 \in ℕ_{0}$
172		2nn	$⊢ 2 \in ℕ$
173		1lt2	$⊢ 1 < 2$
174		elfzo0	$⊢ 1 \in (0 ..^2) \leftrightarrow (1 \in ℕ_{0} \land 2 \in ℕ \land 1 < 2)$
175	171 172 173 174	mpbir3an	$⊢ 1 \in (0 ..^2)$
176	155	oveq2i	$⊢ (0 ..^\|⟨“ r s ”⟩\|) = (0 ..^2)$
177	175 176	eleqtrri	$⊢ 1 \in (0 ..^\|⟨“ r s ”⟩\|)$
178	177	a1i	$⊢ (φ \land (r \in T \land s \in T)) \to 1 \in (0 ..^\|⟨“ r s ”⟩\|)$
179	119 152 153 122 178	splfv2a	$⊢ (φ \land (r \in T \land s \in T)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) = ⟨“ r s ”⟩ (1)$
180		s2fv1	$⊢ s \in T \to ⟨“ r s ”⟩ (1) = s$
181	180	ad2antll	$⊢ (φ \land (r \in T \land s \in T)) \to ⟨“ r s ”⟩ (1) = s$
182	179 181	eqtrd	$⊢ (φ \land (r \in T \land s \in T)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) = s$
183	182	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$
184	183	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$
185	184	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)$
186	170 185	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)$
187		fzosplitsni	$⊢ I \in ℤ_{\geq 0} \to (j \in (0 ..^I + 1) \leftrightarrow (j \in (0 ..^I) \lor j = I))$
188		nn0uz	$⊢ ℕ_{0} = ℤ_{\geq 0}$
189	187 188	eleq2s	$⊢ I \in ℕ_{0} \to (j \in (0 ..^I + 1) \leftrightarrow (j \in (0 ..^I) \lor j = I))$
190	18 189	syl	$⊢ φ \to (j \in (0 ..^I + 1) \leftrightarrow (j \in (0 ..^I) \lor j = I))$
191	190	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))$
192		fveq2	$⊢ k = j \to W (k) = W (j)$
193	192	difeq1d	$⊢ k = j \to W (k) ∖ I = W (j) ∖ I$
194	193	dmeqd	$⊢ k = j \to dom (W (k) ∖ I) = dom (W (j) ∖ I)$
195	194	eleq2d	$⊢ k = j \to (A \in dom (W (k) ∖ I) \leftrightarrow A \in dom (W (j) ∖ I))$
196	195	notbid	$⊢ k = j \to (\neg A \in dom (W (k) ∖ I) \leftrightarrow \neg A \in dom (W (j) ∖ I))$
197	196	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)$
198	9 197	sylan	$⊢ (φ \land j \in (0 ..^I)) \to \neg A \in dom (W (j) ∖ I)$
199	198	adantlr	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to \neg A \in dom (W (j) ∖ I)$
200	4	ad2antrr	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to W \in Word T$
201	26	ad2antrr	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to I \in (0 \dots I + 2)$
202	37	ad2antrr	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to I + 2 \in (0 \dots \|W\|)$
203	122	adantr	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to ⟨“ r s ”⟩ \in Word T$
204		simpr	$⊢ ((φ \land (r \in T \land s \in T)) \land j \in (0 ..^I)) \to j \in (0 ..^I)$
205	200 201 202 203 204	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)$
206	205	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$
207	206	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)$
208	199 207	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)$
209	208	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))$
210	209	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))$
211		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)$
212		0nn0	$⊢ 0 \in ℕ_{0}$
213		2pos	$⊢ 0 < 2$
214		elfzo0	$⊢ 0 \in (0 ..^2) \leftrightarrow (0 \in ℕ_{0} \land 2 \in ℕ \land 0 < 2)$
215	212 172 213 214	mpbir3an	$⊢ 0 \in (0 ..^2)$
216	215 176	eleqtrri	$⊢ 0 \in (0 ..^\|⟨“ r s ”⟩\|)$
217	216	a1i	$⊢ (φ \land (r \in T \land s \in T)) \to 0 \in (0 ..^\|⟨“ r s ”⟩\|)$
218	119 152 153 122 217	splfv2a	$⊢ (φ \land (r \in T \land s \in T)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 0) = ⟨“ r s ”⟩ (0)$
219	32	addid1d	$⊢ φ \to I + 0 = I$
220	219	adantr	$⊢ (φ \land (r \in T \land s \in T)) \to I + 0 = I$
221	220	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)$
222		s2fv0	$⊢ r \in T \to ⟨“ r s ”⟩ (0) = r$
223	222	ad2antrl	$⊢ (φ \land (r \in T \land s \in T)) \to ⟨“ r s ”⟩ (0) = r$
224	218 221 223	3eqtr3d	$⊢ (φ \land (r \in T \land s \in T)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) = r$
225	224	difeq1d	$⊢ (φ \land (r \in T \land s \in T)) \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I = r ∖ I$
226	225	dmeqd	$⊢ (φ \land (r \in T \land s \in T)) \to dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I) = dom (r ∖ I)$
227	226	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))$
228	227	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))$
229	211 228	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)$
230		fveq2	$⊢ j = I \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I)$
231	230	difeq1d	$⊢ j = I \to (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I$
232	231	dmeqd	$⊢ j = I \to dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I) = dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I) ∖ I)$
233	232	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))$
234	233	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))$
235	229 234	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))$
236	210 235	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))$
237	191 236	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))$
238	237	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)$
239	169 186 238	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))$
240		oveq2	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to \sum_{G} w = \sum_{G} (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩)$
241	240	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})$
242		fveqeq2	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to (\|w\| = L \leftrightarrow \|W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩\| = L)$
243	241 242	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))$
244		fveq1	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to w (I + 1) = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1)$
245	244	difeq1d	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to w (I + 1) ∖ I = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (I + 1) ∖ I$
246	245	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)$
247	246	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))$
248		fveq1	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to w (j) = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j)$
249	248	difeq1d	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to w (j) ∖ I = (W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I$
250	249	dmeqd	$⊢ w = W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩ \to dom (w (j) ∖ I) = dom ((W splice ⟨I, I + 2, ⟨“ r s ”⟩⟩) (j) ∖ I)$
251	250	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))$
252	251	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))$
253	252	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))$
254	247 253	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)))$
255	243 254	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))))$
256	255	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)))$
257	125 168 239 256	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)))$
258	257	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))))$
259	258	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))))$
260	2 3 88 90 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)))$
261	118 259 260	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