Metamath Proof Explorer

Theorem cats1un

Description: Express a word with an extra symbol as the union of the word and the new value. (Contributed by Mario Carneiro, 28-Feb-2016)

Ref Expression
Assertion cats1un 
|- ( ( A e. Word X /\ B e. X ) -> ( A ++ <" B "> ) = ( A u. { <. ( # ` A ) , B >. } ) )

Proof

Step Hyp Ref Expression
1 ccatws1cl 
 |-  ( ( A e. Word X /\ B e. X ) -> ( A ++ <" B "> ) e. Word X )
2 wrdf 
 |-  ( ( A ++ <" B "> ) e. Word X -> ( A ++ <" B "> ) : ( 0 ..^ ( # ` ( A ++ <" B "> ) ) ) --> X )
3 1 2 syl 
 |-  ( ( A e. Word X /\ B e. X ) -> ( A ++ <" B "> ) : ( 0 ..^ ( # ` ( A ++ <" B "> ) ) ) --> X )
4 ccatws1len 
 |-  ( A e. Word X -> ( # ` ( A ++ <" B "> ) ) = ( ( # ` A ) + 1 ) )
5 4 oveq2d 
 |-  ( A e. Word X -> ( 0 ..^ ( # ` ( A ++ <" B "> ) ) ) = ( 0 ..^ ( ( # ` A ) + 1 ) ) )
6 lencl 
 |-  ( A e. Word X -> ( # ` A ) e. NN0 )
7 nn0uz 
 |-  NN0 = ( ZZ>= ` 0 )
8 6 7 eleqtrdi 
 |-  ( A e. Word X -> ( # ` A ) e. ( ZZ>= ` 0 ) )
9 fzosplitsn 
 |-  ( ( # ` A ) e. ( ZZ>= ` 0 ) -> ( 0 ..^ ( ( # ` A ) + 1 ) ) = ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) )
10 8 9 syl 
 |-  ( A e. Word X -> ( 0 ..^ ( ( # ` A ) + 1 ) ) = ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) )
11 5 10 eqtrd 
 |-  ( A e. Word X -> ( 0 ..^ ( # ` ( A ++ <" B "> ) ) ) = ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) )
12 11 adantr 
 |-  ( ( A e. Word X /\ B e. X ) -> ( 0 ..^ ( # ` ( A ++ <" B "> ) ) ) = ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) )
13 12 feq2d 
 |-  ( ( A e. Word X /\ B e. X ) -> ( ( A ++ <" B "> ) : ( 0 ..^ ( # ` ( A ++ <" B "> ) ) ) --> X <-> ( A ++ <" B "> ) : ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) --> X ) )
14 3 13 mpbid 
 |-  ( ( A e. Word X /\ B e. X ) -> ( A ++ <" B "> ) : ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) --> X )
15 14 ffnd 
 |-  ( ( A e. Word X /\ B e. X ) -> ( A ++ <" B "> ) Fn ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) )
16 wrdf 
 |-  ( A e. Word X -> A : ( 0 ..^ ( # ` A ) ) --> X )
17 16 adantr 
 |-  ( ( A e. Word X /\ B e. X ) -> A : ( 0 ..^ ( # ` A ) ) --> X )
18 eqid 
 |-  { <. ( # ` A ) , B >. } = { <. ( # ` A ) , B >. }
19 fsng 
 |-  ( ( ( # ` A ) e. NN0 /\ B e. X ) -> ( { <. ( # ` A ) , B >. } : { ( # ` A ) } --> { B } <-> { <. ( # ` A ) , B >. } = { <. ( # ` A ) , B >. } ) )
20 18 19 mpbiri 
 |-  ( ( ( # ` A ) e. NN0 /\ B e. X ) -> { <. ( # ` A ) , B >. } : { ( # ` A ) } --> { B } )
21 6 20 sylan 
 |-  ( ( A e. Word X /\ B e. X ) -> { <. ( # ` A ) , B >. } : { ( # ` A ) } --> { B } )
22 fzodisjsn 
 |-  ( ( 0 ..^ ( # ` A ) ) i^i { ( # ` A ) } ) = (/)
23 22 a1i 
 |-  ( ( A e. Word X /\ B e. X ) -> ( ( 0 ..^ ( # ` A ) ) i^i { ( # ` A ) } ) = (/) )
24 fun 
 |-  ( ( ( A : ( 0 ..^ ( # ` A ) ) --> X /\ { <. ( # ` A ) , B >. } : { ( # ` A ) } --> { B } ) /\ ( ( 0 ..^ ( # ` A ) ) i^i { ( # ` A ) } ) = (/) ) -> ( A u. { <. ( # ` A ) , B >. } ) : ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) --> ( X u. { B } ) )
25 17 21 23 24 syl21anc 
 |-  ( ( A e. Word X /\ B e. X ) -> ( A u. { <. ( # ` A ) , B >. } ) : ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) --> ( X u. { B } ) )
26 25 ffnd 
 |-  ( ( A e. Word X /\ B e. X ) -> ( A u. { <. ( # ` A ) , B >. } ) Fn ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) )
27 elun 
 |-  ( x e. ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) <-> ( x e. ( 0 ..^ ( # ` A ) ) \/ x e. { ( # ` A ) } ) )
28 ccats1val1 
 |-  ( ( A e. Word X /\ x e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ <" B "> ) ` x ) = ( A ` x ) )
29 28 adantlr 
 |-  ( ( ( A e. Word X /\ B e. X ) /\ x e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ <" B "> ) ` x ) = ( A ` x ) )
30 simpr 
 |-  ( ( ( A e. Word X /\ B e. X ) /\ x e. ( 0 ..^ ( # ` A ) ) ) -> x e. ( 0 ..^ ( # ` A ) ) )
31 fzonel 
 |-  -. ( # ` A ) e. ( 0 ..^ ( # ` A ) )
32 nelne2 
 |-  ( ( x e. ( 0 ..^ ( # ` A ) ) /\ -. ( # ` A ) e. ( 0 ..^ ( # ` A ) ) ) -> x =/= ( # ` A ) )
33 30 31 32 sylancl 
 |-  ( ( ( A e. Word X /\ B e. X ) /\ x e. ( 0 ..^ ( # ` A ) ) ) -> x =/= ( # ` A ) )
34 33 necomd 
 |-  ( ( ( A e. Word X /\ B e. X ) /\ x e. ( 0 ..^ ( # ` A ) ) ) -> ( # ` A ) =/= x )
35 fvunsn 
 |-  ( ( # ` A ) =/= x -> ( ( A u. { <. ( # ` A ) , B >. } ) ` x ) = ( A ` x ) )
36 34 35 syl 
 |-  ( ( ( A e. Word X /\ B e. X ) /\ x e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A u. { <. ( # ` A ) , B >. } ) ` x ) = ( A ` x ) )
37 29 36 eqtr4d 
 |-  ( ( ( A e. Word X /\ B e. X ) /\ x e. ( 0 ..^ ( # ` A ) ) ) -> ( ( A ++ <" B "> ) ` x ) = ( ( A u. { <. ( # ` A ) , B >. } ) ` x ) )
38 fvexd 
 |-  ( ( A e. Word X /\ B e. X ) -> ( # ` A ) e. _V )
39 simpr 
 |-  ( ( A e. Word X /\ B e. X ) -> B e. X )
40 17 fdmd 
 |-  ( ( A e. Word X /\ B e. X ) -> dom A = ( 0 ..^ ( # ` A ) ) )
41 40 eleq2d 
 |-  ( ( A e. Word X /\ B e. X ) -> ( ( # ` A ) e. dom A <-> ( # ` A ) e. ( 0 ..^ ( # ` A ) ) ) )
42 31 41 mtbiri 
 |-  ( ( A e. Word X /\ B e. X ) -> -. ( # ` A ) e. dom A )
43 fsnunfv 
 |-  ( ( ( # ` A ) e. _V /\ B e. X /\ -. ( # ` A ) e. dom A ) -> ( ( A u. { <. ( # ` A ) , B >. } ) ` ( # ` A ) ) = B )
44 38 39 42 43 syl3anc 
 |-  ( ( A e. Word X /\ B e. X ) -> ( ( A u. { <. ( # ` A ) , B >. } ) ` ( # ` A ) ) = B )
45 simpl 
 |-  ( ( A e. Word X /\ B e. X ) -> A e. Word X )
46 s1cl 
 |-  ( B e. X -> <" B "> e. Word X )
47 46 adantl 
 |-  ( ( A e. Word X /\ B e. X ) -> <" B "> e. Word X )
48 s1len 
 |-  ( # ` <" B "> ) = 1
49 1nn 
 |-  1 e. NN
50 48 49 eqeltri 
 |-  ( # ` <" B "> ) e. NN
51 lbfzo0 
 |-  ( 0 e. ( 0 ..^ ( # ` <" B "> ) ) <-> ( # ` <" B "> ) e. NN )
52 50 51 mpbir 
 |-  0 e. ( 0 ..^ ( # ` <" B "> ) )
53 52 a1i 
 |-  ( ( A e. Word X /\ B e. X ) -> 0 e. ( 0 ..^ ( # ` <" B "> ) ) )
54 ccatval3 
 |-  ( ( A e. Word X /\ <" B "> e. Word X /\ 0 e. ( 0 ..^ ( # ` <" B "> ) ) ) -> ( ( A ++ <" B "> ) ` ( 0 + ( # ` A ) ) ) = ( <" B "> ` 0 ) )
55 45 47 53 54 syl3anc 
 |-  ( ( A e. Word X /\ B e. X ) -> ( ( A ++ <" B "> ) ` ( 0 + ( # ` A ) ) ) = ( <" B "> ` 0 ) )
56 s1fv 
 |-  ( B e. X -> ( <" B "> ` 0 ) = B )
57 56 adantl 
 |-  ( ( A e. Word X /\ B e. X ) -> ( <" B "> ` 0 ) = B )
58 55 57 eqtrd 
 |-  ( ( A e. Word X /\ B e. X ) -> ( ( A ++ <" B "> ) ` ( 0 + ( # ` A ) ) ) = B )
59 6 adantr 
 |-  ( ( A e. Word X /\ B e. X ) -> ( # ` A ) e. NN0 )
60 59 nn0cnd 
 |-  ( ( A e. Word X /\ B e. X ) -> ( # ` A ) e. CC )
61 60 addlidd 
 |-  ( ( A e. Word X /\ B e. X ) -> ( 0 + ( # ` A ) ) = ( # ` A ) )
62 61 fveq2d 
 |-  ( ( A e. Word X /\ B e. X ) -> ( ( A ++ <" B "> ) ` ( 0 + ( # ` A ) ) ) = ( ( A ++ <" B "> ) ` ( # ` A ) ) )
63 44 58 62 3eqtr2rd 
 |-  ( ( A e. Word X /\ B e. X ) -> ( ( A ++ <" B "> ) ` ( # ` A ) ) = ( ( A u. { <. ( # ` A ) , B >. } ) ` ( # ` A ) ) )
64 elsni 
 |-  ( x e. { ( # ` A ) } -> x = ( # ` A ) )
65 64 fveq2d 
 |-  ( x e. { ( # ` A ) } -> ( ( A ++ <" B "> ) ` x ) = ( ( A ++ <" B "> ) ` ( # ` A ) ) )
66 64 fveq2d 
 |-  ( x e. { ( # ` A ) } -> ( ( A u. { <. ( # ` A ) , B >. } ) ` x ) = ( ( A u. { <. ( # ` A ) , B >. } ) ` ( # ` A ) ) )
67 65 66 eqeq12d 
 |-  ( x e. { ( # ` A ) } -> ( ( ( A ++ <" B "> ) ` x ) = ( ( A u. { <. ( # ` A ) , B >. } ) ` x ) <-> ( ( A ++ <" B "> ) ` ( # ` A ) ) = ( ( A u. { <. ( # ` A ) , B >. } ) ` ( # ` A ) ) ) )
68 63 67 syl5ibrcom 
 |-  ( ( A e. Word X /\ B e. X ) -> ( x e. { ( # ` A ) } -> ( ( A ++ <" B "> ) ` x ) = ( ( A u. { <. ( # ` A ) , B >. } ) ` x ) ) )
69 68 imp 
 |-  ( ( ( A e. Word X /\ B e. X ) /\ x e. { ( # ` A ) } ) -> ( ( A ++ <" B "> ) ` x ) = ( ( A u. { <. ( # ` A ) , B >. } ) ` x ) )
70 37 69 jaodan 
 |-  ( ( ( A e. Word X /\ B e. X ) /\ ( x e. ( 0 ..^ ( # ` A ) ) \/ x e. { ( # ` A ) } ) ) -> ( ( A ++ <" B "> ) ` x ) = ( ( A u. { <. ( # ` A ) , B >. } ) ` x ) )
71 27 70 sylan2b 
 |-  ( ( ( A e. Word X /\ B e. X ) /\ x e. ( ( 0 ..^ ( # ` A ) ) u. { ( # ` A ) } ) ) -> ( ( A ++ <" B "> ) ` x ) = ( ( A u. { <. ( # ` A ) , B >. } ) ` x ) )
72 15 26 71 eqfnfvd 
 |-  ( ( A e. Word X /\ B e. X ) -> ( A ++ <" B "> ) = ( A u. { <. ( # ` A ) , B >. } ) )