Metamath Proof Explorer

Theorem repsdf2

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

Ref Expression
Assertion repsdf2 ( ( 𝑆 ∈ 𝑉 ∧ 𝑁 ∈ ℕ0 ) → ( 𝑊 = ( 𝑆 repeatS 𝑁 ) ↔ ( 𝑊 ∈ Word 𝑉 ∧ ( ♯ ‘ 𝑊 ) = 𝑁 ∧ ∀ 𝑖 ∈ ( 0 ..^ 𝑁 ) ( 𝑊 ‘ 𝑖 ) = 𝑆 ) ) )

Proof

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