wrdind

Description: Perform induction over the structure of a word. (Contributed by Mario Carneiro, 27-Sep-2015) (Revised by Mario Carneiro, 26-Feb-2016) (Proof shortened by AV, 12-Oct-2022)

	Ref	Expression
Hypotheses	wrdind.1	$⊢ x = \emptyset \to (φ \leftrightarrow ψ)$
	wrdind.2	$⊢ x = y \to (φ \leftrightarrow χ)$
	wrdind.3	$⊢ x = y ++ ⟨“ z ”⟩ \to (φ \leftrightarrow θ)$
	wrdind.4	$⊢ x = A \to (φ \leftrightarrow τ)$
	wrdind.5	$⊢ ψ$
	wrdind.6	$⊢ (y \in Word B \land z \in B) \to (χ \to θ)$
Assertion	wrdind	$⊢ A \in Word B \to τ$

Proof

Step	Hyp	Ref	Expression
1		wrdind.1	$⊢ x = \emptyset \to (φ \leftrightarrow ψ)$
2		wrdind.2	$⊢ x = y \to (φ \leftrightarrow χ)$
3		wrdind.3	$⊢ x = y ++ ⟨“ z ”⟩ \to (φ \leftrightarrow θ)$
4		wrdind.4	$⊢ x = A \to (φ \leftrightarrow τ)$
5		wrdind.5	$⊢ ψ$
6		wrdind.6	$⊢ (y \in Word B \land z \in B) \to (χ \to θ)$
7		lencl	$⊢ A \in Word B \to \|A\| \in ℕ_{0}$
8		eqeq2	$⊢ n = 0 \to (\|x\| = n \leftrightarrow \|x\| = 0)$
9	8	imbi1d	$⊢ n = 0 \to ((\|x\| = n \to φ) \leftrightarrow (\|x\| = 0 \to φ))$
10	9	ralbidv	$⊢ n = 0 \to (\forall x \in Word B (\|x\| = n \to φ) \leftrightarrow \forall x \in Word B (\|x\| = 0 \to φ))$
11		eqeq2	$⊢ n = m \to (\|x\| = n \leftrightarrow \|x\| = m)$
12	11	imbi1d	$⊢ n = m \to ((\|x\| = n \to φ) \leftrightarrow (\|x\| = m \to φ))$
13	12	ralbidv	$⊢ n = m \to (\forall x \in Word B (\|x\| = n \to φ) \leftrightarrow \forall x \in Word B (\|x\| = m \to φ))$
14		eqeq2	$⊢ n = m + 1 \to (\|x\| = n \leftrightarrow \|x\| = m + 1)$
15	14	imbi1d	$⊢ n = m + 1 \to ((\|x\| = n \to φ) \leftrightarrow (\|x\| = m + 1 \to φ))$
16	15	ralbidv	$⊢ n = m + 1 \to (\forall x \in Word B (\|x\| = n \to φ) \leftrightarrow \forall x \in Word B (\|x\| = m + 1 \to φ))$
17		eqeq2	$⊢ n = \|A\| \to (\|x\| = n \leftrightarrow \|x\| = \|A\|)$
18	17	imbi1d	$⊢ n = \|A\| \to ((\|x\| = n \to φ) \leftrightarrow (\|x\| = \|A\| \to φ))$
19	18	ralbidv	$⊢ n = \|A\| \to (\forall x \in Word B (\|x\| = n \to φ) \leftrightarrow \forall x \in Word B (\|x\| = \|A\| \to φ))$
20		hasheq0	$⊢ x \in Word B \to (\|x\| = 0 \leftrightarrow x = \emptyset)$
21	5 1	mpbiri	$⊢ x = \emptyset \to φ$
22	20 21	biimtrdi	$⊢ x \in Word B \to (\|x\| = 0 \to φ)$
23	22	rgen	$⊢ \forall x \in Word B (\|x\| = 0 \to φ)$
24		fveqeq2	$⊢ x = y \to (\|x\| = m \leftrightarrow \|y\| = m)$
25	24 2	imbi12d	$⊢ x = y \to ((\|x\| = m \to φ) \leftrightarrow (\|y\| = m \to χ))$
26	25	cbvralvw	$⊢ \forall x \in Word B (\|x\| = m \to φ) \leftrightarrow \forall y \in Word B (\|y\| = m \to χ)$
27		simprl	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to x \in Word B$
28		fzossfz	$⊢ (0 ..^\|x\|) \subseteq (0 \dots \|x\|)$
29		simprr	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to \|x\| = m + 1$
30		nn0p1nn	$⊢ m \in ℕ_{0} \to m + 1 \in ℕ$
31	30	ad2antrr	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to m + 1 \in ℕ$
32	29 31	eqeltrd	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to \|x\| \in ℕ$
33		fzo0end	$⊢ \|x\| \in ℕ \to \|x\| - 1 \in (0 ..^\|x\|)$
34	32 33	syl	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to \|x\| - 1 \in (0 ..^\|x\|)$
35	28 34	sselid	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to \|x\| - 1 \in (0 \dots \|x\|)$
36		pfxlen	$⊢ (x \in Word B \land \|x\| - 1 \in (0 \dots \|x\|)) \to \|x prefix (\|x\| - 1)\| = \|x\| - 1$
37	27 35 36	syl2anc	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to \|x prefix (\|x\| - 1)\| = \|x\| - 1$
38	29	oveq1d	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to \|x\| - 1 = m + 1 - 1$
39		nn0cn	$⊢ m \in ℕ_{0} \to m \in ℂ$
40	39	ad2antrr	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to m \in ℂ$
41		ax-1cn	$⊢ 1 \in ℂ$
42		pncan	$⊢ (m \in ℂ \land 1 \in ℂ) \to m + 1 - 1 = m$
43	40 41 42	sylancl	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to m + 1 - 1 = m$
44	37 38 43	3eqtrd	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to \|x prefix (\|x\| - 1)\| = m$
45		fveqeq2	$⊢ y = x prefix (\|x\| - 1) \to (\|y\| = m \leftrightarrow \|x prefix (\|x\| - 1)\| = m)$
46		vex	$⊢ y \in V$
47	46 2	sbcie	$⊢ \underset{˙}{[} y / x \underset{˙}{]} φ \leftrightarrow χ$
48		dfsbcq	$⊢ y = x prefix (\|x\| - 1) \to (\underset{˙}{[} y / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} φ)$
49	47 48	bitr3id	$⊢ y = x prefix (\|x\| - 1) \to (χ \leftrightarrow \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} φ)$
50	45 49	imbi12d	$⊢ y = x prefix (\|x\| - 1) \to ((\|y\| = m \to χ) \leftrightarrow (\|x prefix (\|x\| - 1)\| = m \to \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} φ))$
51		simplr	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to \forall y \in Word B (\|y\| = m \to χ)$
52		pfxcl	$⊢ x \in Word B \to x prefix (\|x\| - 1) \in Word B$
53	52	ad2antrl	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to x prefix (\|x\| - 1) \in Word B$
54	50 51 53	rspcdva	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to (\|x prefix (\|x\| - 1)\| = m \to \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} φ)$
55	44 54	mpd	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to \underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} φ$
56	32	nnge1d	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to 1 \leq \|x\|$
57		wrdlenge1n0	$⊢ x \in Word B \to (x \neq \emptyset \leftrightarrow 1 \leq \|x\|)$
58	57	ad2antrl	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to (x \neq \emptyset \leftrightarrow 1 \leq \|x\|)$
59	56 58	mpbird	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to x \neq \emptyset$
60		lswcl	$⊢ (x \in Word B \land x \neq \emptyset) \to lastS (x) \in B$
61	27 59 60	syl2anc	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to lastS (x) \in B$
62		oveq1	$⊢ y = x prefix (\|x\| - 1) \to y ++ ⟨“ z ”⟩ = (x prefix (\|x\| - 1)) ++ ⟨“ z ”⟩$
63	62	sbceq1d	$⊢ y = x prefix (\|x\| - 1) \to (\underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ)$
64	48 63	imbi12d	$⊢ y = x prefix (\|x\| - 1) \to ((\underset{˙}{[} y / x \underset{˙}{]} φ \to \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ) \leftrightarrow (\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} φ \to \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ))$
65		s1eq	$⊢ z = lastS (x) \to ⟨“ z ”⟩ = ⟨“ lastS (x) ”⟩$
66	65	oveq2d	$⊢ z = lastS (x) \to (x prefix (\|x\| - 1)) ++ ⟨“ z ”⟩ = (x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩$
67	66	sbceq1d	$⊢ z = lastS (x) \to (\underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} φ)$
68	67	imbi2d	$⊢ z = lastS (x) \to ((\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} φ \to \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ) \leftrightarrow (\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} φ \to \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} φ))$
69		ovex	$⊢ y ++ ⟨“ z ”⟩ \in V$
70	69 3	sbcie	$⊢ \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ \leftrightarrow θ$
71	6 47 70	3imtr4g	$⊢ (y \in Word B \land z \in B) \to (\underset{˙}{[} y / x \underset{˙}{]} φ \to \underset{˙}{[} (y ++ ⟨“ z ”⟩) / x \underset{˙}{]} φ)$
72	64 68 71	vtocl2ga	$⊢ (x prefix (\|x\| - 1) \in Word B \land lastS (x) \in B) \to (\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} φ \to \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} φ)$
73	53 61 72	syl2anc	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to (\underset{˙}{[} (x prefix (\|x\| - 1)) / x \underset{˙}{]} φ \to \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} φ)$
74	55 73	mpd	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} φ$
75		wrdfin	$⊢ x \in Word B \to x \in Fin$
76	75	ad2antrl	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to x \in Fin$
77		hashnncl	$⊢ x \in Fin \to (\|x\| \in ℕ \leftrightarrow x \neq \emptyset)$
78	76 77	syl	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to (\|x\| \in ℕ \leftrightarrow x \neq \emptyset)$
79	32 78	mpbid	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to x \neq \emptyset$
80		pfxlswccat	$⊢ (x \in Word B \land x \neq \emptyset) \to (x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩ = x$
81	80	eqcomd	$⊢ (x \in Word B \land x \neq \emptyset) \to x = (x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩$
82	27 79 81	syl2anc	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to x = (x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩$
83		sbceq1a	$⊢ x = (x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩ \to (φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} φ)$
84	82 83	syl	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to (φ \leftrightarrow \underset{˙}{[} ((x prefix (\|x\| - 1)) ++ ⟨“ lastS (x) ”⟩) / x \underset{˙}{]} φ)$
85	74 84	mpbird	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land (x \in Word B \land \|x\| = m + 1)) \to φ$
86	85	expr	$⊢ ((m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \land x \in Word B) \to (\|x\| = m + 1 \to φ)$
87	86	ralrimiva	$⊢ (m \in ℕ_{0} \land \forall y \in Word B (\|y\| = m \to χ)) \to \forall x \in Word B (\|x\| = m + 1 \to φ)$
88	87	ex	$⊢ m \in ℕ_{0} \to (\forall y \in Word B (\|y\| = m \to χ) \to \forall x \in Word B (\|x\| = m + 1 \to φ))$
89	26 88	biimtrid	$⊢ m \in ℕ_{0} \to (\forall x \in Word B (\|x\| = m \to φ) \to \forall x \in Word B (\|x\| = m + 1 \to φ))$
90	10 13 16 19 23 89	nn0ind	$⊢ \|A\| \in ℕ_{0} \to \forall x \in Word B (\|x\| = \|A\| \to φ)$
91	7 90	syl	$⊢ A \in Word B \to \forall x \in Word B (\|x\| = \|A\| \to φ)$
92		eqidd	$⊢ A \in Word B \to \|A\| = \|A\|$
93		fveqeq2	$⊢ x = A \to (\|x\| = \|A\| \leftrightarrow \|A\| = \|A\|)$
94	93 4	imbi12d	$⊢ x = A \to ((\|x\| = \|A\| \to φ) \leftrightarrow (\|A\| = \|A\| \to τ))$
95	94	rspcv	$⊢ A \in Word B \to (\forall x \in Word B (\|x\| = \|A\| \to φ) \to (\|A\| = \|A\| \to τ))$
96	91 92 95	mp2d	$⊢ A \in Word B \to τ$

Metamath Proof Explorer

Theorem wrdind

Proof