Metamath Proof Explorer

Theorem repsdf2

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

Ref Expression
Assertion repsdf2 ⊢ S ∈ V ∧ N ∈ ℕ 0 → W = S repeatS N ↔ W ∈ Word V ∧ W = N ∧ ∀ i ∈ 0 ..^ N W ⁡ i = S

Proof

Step Hyp Ref Expression
1 repsconst ⊢ S ∈ V ∧ N ∈ ℕ 0 → S repeatS N = 0 ..^ N × S
2 1 eqeq2d ⊢ S ∈ V ∧ N ∈ ℕ 0 → W = S repeatS N ↔ W = 0 ..^ N × S
3 fconst2g ⊢ S ∈ V → W : 0 ..^ N ⟶ S ↔ W = 0 ..^ N × S
4 3 adantr ⊢ S ∈ V ∧ N ∈ ℕ 0 → W : 0 ..^ N ⟶ S ↔ W = 0 ..^ N × S
5 fconstfv ⊢ W : 0 ..^ N ⟶ S ↔ W Fn 0 ..^ N ∧ ∀ i ∈ 0 ..^ N W ⁡ i = S
6 snssi ⊢ S ∈ V → S ⊆ V
7 6 adantr ⊢ S ∈ V ∧ N ∈ ℕ 0 → S ⊆ V
8 7 anim1ci ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ W : 0 ..^ N ⟶ S → W : 0 ..^ N ⟶ S ∧ S ⊆ V
9 fss ⊢ W : 0 ..^ N ⟶ S ∧ S ⊆ V → W : 0 ..^ N ⟶ V
10 iswrdi ⊢ W : 0 ..^ N ⟶ V → W ∈ Word V
11 8 9 10 3syl ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ W : 0 ..^ N ⟶ S → W ∈ Word V
12 ffzo0hash ⊢ N ∈ ℕ 0 ∧ W Fn 0 ..^ N → W = N
13 12 expcom ⊢ W Fn 0 ..^ N → N ∈ ℕ 0 → W = N
14 ffn ⊢ W : 0 ..^ N ⟶ S → W Fn 0 ..^ N
15 13 14 syl11 ⊢ N ∈ ℕ 0 → W : 0 ..^ N ⟶ S → W = N
16 15 adantl ⊢ S ∈ V ∧ N ∈ ℕ 0 → W : 0 ..^ N ⟶ S → W = N
17 16 imp ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ W : 0 ..^ N ⟶ S → W = N
18 11 17 jca ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ W : 0 ..^ N ⟶ S → W ∈ Word V ∧ W = N
19 18 ex ⊢ S ∈ V ∧ N ∈ ℕ 0 → W : 0 ..^ N ⟶ S → W ∈ Word V ∧ W = N
20 5 19 syl5bir ⊢ S ∈ V ∧ N ∈ ℕ 0 → W Fn 0 ..^ N ∧ ∀ i ∈ 0 ..^ N W ⁡ i = S → W ∈ Word V ∧ W = N
21 20 expcomd ⊢ S ∈ V ∧ N ∈ ℕ 0 → ∀ i ∈ 0 ..^ N W ⁡ i = S → W Fn 0 ..^ N → W ∈ Word V ∧ W = N
22 21 imp ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ ∀ i ∈ 0 ..^ N W ⁡ i = S → W Fn 0 ..^ N → W ∈ Word V ∧ W = N
23 wrdf ⊢ W ∈ Word V → W : 0 ..^ W ⟶ V
24 ffn ⊢ W : 0 ..^ W ⟶ V → W Fn 0 ..^ W
25 oveq2 ⊢ W = N → 0 ..^ W = 0 ..^ N
26 25 fneq2d ⊢ W = N → W Fn 0 ..^ W ↔ W Fn 0 ..^ N
27 26 biimpd ⊢ W = N → W Fn 0 ..^ W → W Fn 0 ..^ N
28 27 a1d ⊢ W = N → S ∈ V ∧ N ∈ ℕ 0 → W Fn 0 ..^ W → W Fn 0 ..^ N
29 28 com13 ⊢ W Fn 0 ..^ W → S ∈ V ∧ N ∈ ℕ 0 → W = N → W Fn 0 ..^ N
30 23 24 29 3syl ⊢ W ∈ Word V → S ∈ V ∧ N ∈ ℕ 0 → W = N → W Fn 0 ..^ N
31 30 com12 ⊢ S ∈ V ∧ N ∈ ℕ 0 → W ∈ Word V → W = N → W Fn 0 ..^ N
32 31 impd ⊢ S ∈ V ∧ N ∈ ℕ 0 → W ∈ Word V ∧ W = N → W Fn 0 ..^ N
33 32 adantr ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ ∀ i ∈ 0 ..^ N W ⁡ i = S → W ∈ Word V ∧ W = N → W Fn 0 ..^ N
34 22 33 impbid ⊢ S ∈ V ∧ N ∈ ℕ 0 ∧ ∀ i ∈ 0 ..^ N W ⁡ i = S → W Fn 0 ..^ N ↔ W ∈ Word V ∧ W = N
35 34 ex ⊢ S ∈ V ∧ N ∈ ℕ 0 → ∀ i ∈ 0 ..^ N W ⁡ i = S → W Fn 0 ..^ N ↔ W ∈ Word V ∧ W = N
36 35 pm5.32rd ⊢ S ∈ V ∧ N ∈ ℕ 0 → W Fn 0 ..^ N ∧ ∀ i ∈ 0 ..^ N W ⁡ i = S ↔ W ∈ Word V ∧ W = N ∧ ∀ i ∈ 0 ..^ N W ⁡ i = S
37 df-3an ⊢ W ∈ Word V ∧ W = N ∧ ∀ i ∈ 0 ..^ N W ⁡ i = S ↔ W ∈ Word V ∧ W = N ∧ ∀ i ∈ 0 ..^ N W ⁡ i = S
38 36 5 37 3bitr4g ⊢ S ∈ V ∧ N ∈ ℕ 0 → W : 0 ..^ N ⟶ S ↔ W ∈ Word V ∧ W = N ∧ ∀ i ∈ 0 ..^ N W ⁡ i = S
39 2 4 38 3bitr2d ⊢ S ∈ V ∧ N ∈ ℕ 0 → W = S repeatS N ↔ W ∈ Word V ∧ W = N ∧ ∀ i ∈ 0 ..^ N W ⁡ i = S