repsdf2

Description: Alternative definition of a "repeated symbol word". (Contributed by AV, 7-Nov-2018)

		Ref	Expression
	Assertion	repsdf2	$⊢ (S \in V \land N \in ℕ_{0}) \to (W = S repeatS N \leftrightarrow (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = S))$

Proof

Step	Hyp	Ref	Expression
1		repsconst	$⊢ (S \in V \land N \in ℕ_{0}) \to S repeatS N = (0 ..^N) \times \{S\}$
2	1	eqeq2d	$⊢ (S \in V \land N \in ℕ_{0}) \to (W = S repeatS N \leftrightarrow W = (0 ..^N) \times \{S\})$
3		fconst2g	$⊢ S \in V \to (W : (0 ..^N) ⟶ \{S\} \leftrightarrow W = (0 ..^N) \times \{S\})$
4	3	adantr	$⊢ (S \in V \land N \in ℕ_{0}) \to (W : (0 ..^N) ⟶ \{S\} \leftrightarrow W = (0 ..^N) \times \{S\})$
5		fconstfv	$⊢ W : (0 ..^N) ⟶ \{S\} \leftrightarrow (W Fn (0 ..^N) \land \forall i \in (0 ..^N) W (i) = S)$
6		snssi	$⊢ S \in V \to \{S\} \subseteq V$
7	6	adantr	$⊢ (S \in V \land N \in ℕ_{0}) \to \{S\} \subseteq V$
8	7	anim1ci	$⊢ ((S \in V \land N \in ℕ_{0}) \land W : (0 ..^N) ⟶ \{S\}) \to (W : (0 ..^N) ⟶ \{S\} \land \{S\} \subseteq V)$
9		fss	$⊢ (W : (0 ..^N) ⟶ \{S\} \land \{S\} \subseteq V) \to W : (0 ..^N) ⟶ V$
10		iswrdi	$⊢ W : (0 ..^N) ⟶ V \to W \in Word V$
11	8 9 10	3syl	$⊢ ((S \in V \land N \in ℕ_{0}) \land W : (0 ..^N) ⟶ \{S\}) \to W \in Word V$
12		ffzo0hash	$⊢ (N \in ℕ_{0} \land W Fn (0 ..^N)) \to \|W\| = N$
13	12	expcom	$⊢ W Fn (0 ..^N) \to (N \in ℕ_{0} \to \|W\| = N)$
14		ffn	$⊢ W : (0 ..^N) ⟶ \{S\} \to W Fn (0 ..^N)$
15	13 14	syl11	$⊢ N \in ℕ_{0} \to (W : (0 ..^N) ⟶ \{S\} \to \|W\| = N)$
16	15	adantl	$⊢ (S \in V \land N \in ℕ_{0}) \to (W : (0 ..^N) ⟶ \{S\} \to \|W\| = N)$
17	16	imp	$⊢ ((S \in V \land N \in ℕ_{0}) \land W : (0 ..^N) ⟶ \{S\}) \to \|W\| = N$
18	11 17	jca	$⊢ ((S \in V \land N \in ℕ_{0}) \land W : (0 ..^N) ⟶ \{S\}) \to (W \in Word V \land \|W\| = N)$
19	18	ex	$⊢ (S \in V \land N \in ℕ_{0}) \to (W : (0 ..^N) ⟶ \{S\} \to (W \in Word V \land \|W\| = N))$
20	5 19	biimtrrid	$⊢ (S \in V \land N \in ℕ_{0}) \to ((W Fn (0 ..^N) \land \forall i \in (0 ..^N) W (i) = S) \to (W \in Word V \land \|W\| = N))$
21	20	expcomd	$⊢ (S \in V \land N \in ℕ_{0}) \to (\forall i \in (0 ..^N) W (i) = S \to (W Fn (0 ..^N) \to (W \in Word V \land \|W\| = N)))$
22	21	imp	$⊢ ((S \in V \land N \in ℕ_{0}) \land \forall i \in (0 ..^N) W (i) = S) \to (W Fn (0 ..^N) \to (W \in Word V \land \|W\| = N))$
23		wrdf	$⊢ W \in Word V \to W : (0 ..^\|W\|) ⟶ V$
24		ffn	$⊢ W : (0 ..^\|W\|) ⟶ V \to W Fn (0 ..^\|W\|)$
25		oveq2	$⊢ \|W\| = N \to (0 ..^\|W\|) = (0 ..^N)$
26	25	fneq2d	$⊢ \|W\| = N \to (W Fn (0 ..^\|W\|) \leftrightarrow W Fn (0 ..^N))$
27	26	biimpd	$⊢ \|W\| = N \to (W Fn (0 ..^\|W\|) \to W Fn (0 ..^N))$
28	27	a1d	$⊢ \|W\| = N \to ((S \in V \land N \in ℕ_{0}) \to (W Fn (0 ..^\|W\|) \to W Fn (0 ..^N)))$
29	28	com13	$⊢ W Fn (0 ..^\|W\|) \to ((S \in V \land N \in ℕ_{0}) \to (\|W\| = N \to W Fn (0 ..^N)))$
30	23 24 29	3syl	$⊢ W \in Word V \to ((S \in V \land N \in ℕ_{0}) \to (\|W\| = N \to W Fn (0 ..^N)))$
31	30	com12	$⊢ (S \in V \land N \in ℕ_{0}) \to (W \in Word V \to (\|W\| = N \to W Fn (0 ..^N)))$
32	31	impd	$⊢ (S \in V \land N \in ℕ_{0}) \to ((W \in Word V \land \|W\| = N) \to W Fn (0 ..^N))$
33	32	adantr	$⊢ ((S \in V \land N \in ℕ_{0}) \land \forall i \in (0 ..^N) W (i) = S) \to ((W \in Word V \land \|W\| = N) \to W Fn (0 ..^N))$
34	22 33	impbid	$⊢ ((S \in V \land N \in ℕ_{0}) \land \forall i \in (0 ..^N) W (i) = S) \to (W Fn (0 ..^N) \leftrightarrow (W \in Word V \land \|W\| = N))$
35	34	ex	$⊢ (S \in V \land N \in ℕ_{0}) \to (\forall i \in (0 ..^N) W (i) = S \to (W Fn (0 ..^N) \leftrightarrow (W \in Word V \land \|W\| = N)))$
36	35	pm5.32rd	$⊢ (S \in V \land N \in ℕ_{0}) \to ((W Fn (0 ..^N) \land \forall i \in (0 ..^N) W (i) = S) \leftrightarrow ((W \in Word V \land \|W\| = N) \land \forall i \in (0 ..^N) W (i) = S))$
37		df-3an	$⊢ (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = S) \leftrightarrow ((W \in Word V \land \|W\| = N) \land \forall i \in (0 ..^N) W (i) = S)$
38	36 5 37	3bitr4g	$⊢ (S \in V \land N \in ℕ_{0}) \to (W : (0 ..^N) ⟶ \{S\} \leftrightarrow (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = S))$
39	2 4 38	3bitr2d	$⊢ (S \in V \land N \in ℕ_{0}) \to (W = S repeatS N \leftrightarrow (W \in Word V \land \|W\| = N \land \forall i \in (0 ..^N) W (i) = S))$

Metamath Proof Explorer

Theorem repsdf2

Proof