Metamath Proof Explorer

Theorem repsco

Description: Mapping of words commutes with the "repeated symbol" operation. (Contributed by AV, 11-Nov-2018)

Ref Expression
Assertion repsco 
|- ( ( S e. A /\ N e. NN0 /\ F : A --> B ) -> ( F o. ( S repeatS N ) ) = ( ( F ` S ) repeatS N ) )

Proof

Step Hyp Ref Expression
1 simpl1 
 |-  ( ( ( S e. A /\ N e. NN0 /\ F : A --> B ) /\ x e. ( 0 ..^ N ) ) -> S e. A )
2 simpl2 
 |-  ( ( ( S e. A /\ N e. NN0 /\ F : A --> B ) /\ x e. ( 0 ..^ N ) ) -> N e. NN0 )
3 simpr 
 |-  ( ( ( S e. A /\ N e. NN0 /\ F : A --> B ) /\ x e. ( 0 ..^ N ) ) -> x e. ( 0 ..^ N ) )
4 repswsymb 
 |-  ( ( S e. A /\ N e. NN0 /\ x e. ( 0 ..^ N ) ) -> ( ( S repeatS N ) ` x ) = S )
5 1 2 3 4 syl3anc 
 |-  ( ( ( S e. A /\ N e. NN0 /\ F : A --> B ) /\ x e. ( 0 ..^ N ) ) -> ( ( S repeatS N ) ` x ) = S )
6 5 fveq2d 
 |-  ( ( ( S e. A /\ N e. NN0 /\ F : A --> B ) /\ x e. ( 0 ..^ N ) ) -> ( F ` ( ( S repeatS N ) ` x ) ) = ( F ` S ) )
7 6 mpteq2dva 
 |-  ( ( S e. A /\ N e. NN0 /\ F : A --> B ) -> ( x e. ( 0 ..^ N ) |-> ( F ` ( ( S repeatS N ) ` x ) ) ) = ( x e. ( 0 ..^ N ) |-> ( F ` S ) ) )
8 simp3 
 |-  ( ( S e. A /\ N e. NN0 /\ F : A --> B ) -> F : A --> B )
9 repsf 
 |-  ( ( S e. A /\ N e. NN0 ) -> ( S repeatS N ) : ( 0 ..^ N ) --> A )
10 9 3adant3 
 |-  ( ( S e. A /\ N e. NN0 /\ F : A --> B ) -> ( S repeatS N ) : ( 0 ..^ N ) --> A )
11 fcompt 
 |-  ( ( F : A --> B /\ ( S repeatS N ) : ( 0 ..^ N ) --> A ) -> ( F o. ( S repeatS N ) ) = ( x e. ( 0 ..^ N ) |-> ( F ` ( ( S repeatS N ) ` x ) ) ) )
12 8 10 11 syl2anc 
 |-  ( ( S e. A /\ N e. NN0 /\ F : A --> B ) -> ( F o. ( S repeatS N ) ) = ( x e. ( 0 ..^ N ) |-> ( F ` ( ( S repeatS N ) ` x ) ) ) )
13 fvexd 
 |-  ( S e. A -> ( F ` S ) e. _V )
14 13 anim1i 
 |-  ( ( S e. A /\ N e. NN0 ) -> ( ( F ` S ) e. _V /\ N e. NN0 ) )
15 14 3adant3 
 |-  ( ( S e. A /\ N e. NN0 /\ F : A --> B ) -> ( ( F ` S ) e. _V /\ N e. NN0 ) )
16 reps 
 |-  ( ( ( F ` S ) e. _V /\ N e. NN0 ) -> ( ( F ` S ) repeatS N ) = ( x e. ( 0 ..^ N ) |-> ( F ` S ) ) )
17 15 16 syl 
 |-  ( ( S e. A /\ N e. NN0 /\ F : A --> B ) -> ( ( F ` S ) repeatS N ) = ( x e. ( 0 ..^ N ) |-> ( F ` S ) ) )
18 7 12 17 3eqtr4d 
 |-  ( ( S e. A /\ N e. NN0 /\ F : A --> B ) -> ( F o. ( S repeatS N ) ) = ( ( F ` S ) repeatS N ) )