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 AWordXBXA++⟨“B”⟩=AAB

Proof

Step Hyp Ref Expression
1 ccatws1cl AWordXBXA++⟨“B”⟩WordX
2 wrdf A++⟨“B”⟩WordXA++⟨“B”⟩:0..^A++⟨“B”⟩X
3 1 2 syl AWordXBXA++⟨“B”⟩:0..^A++⟨“B”⟩X
4 ccatws1len AWordXA++⟨“B”⟩=A+1
5 4 oveq2d AWordX0..^A++⟨“B”⟩=0..^A+1
6 lencl AWordXA0
7 nn0uz 0=0
8 6 7 eleqtrdi AWordXA0
9 fzosplitsn A00..^A+1=0..^AA
10 8 9 syl AWordX0..^A+1=0..^AA
11 5 10 eqtrd AWordX0..^A++⟨“B”⟩=0..^AA
12 11 adantr AWordXBX0..^A++⟨“B”⟩=0..^AA
13 12 feq2d AWordXBXA++⟨“B”⟩:0..^A++⟨“B”⟩XA++⟨“B”⟩:0..^AAX
14 3 13 mpbid AWordXBXA++⟨“B”⟩:0..^AAX
15 14 ffnd AWordXBXA++⟨“B”⟩Fn0..^AA
16 wrdf AWordXA:0..^AX
17 16 adantr AWordXBXA:0..^AX
18 eqid AB=AB
19 fsng A0BXAB:ABAB=AB
20 18 19 mpbiri A0BXAB:AB
21 6 20 sylan AWordXBXAB:AB
22 fzodisjsn 0..^AA=
23 22 a1i AWordXBX0..^AA=
24 fun A:0..^AXAB:AB0..^AA=AAB:0..^AAXB
25 17 21 23 24 syl21anc AWordXBXAAB:0..^AAXB
26 25 ffnd AWordXBXAABFn0..^AA
27 elun x0..^AAx0..^AxA
28 ccats1val1 AWordXx0..^AA++⟨“B”⟩x=Ax
29 28 adantlr AWordXBXx0..^AA++⟨“B”⟩x=Ax
30 simpr AWordXBXx0..^Ax0..^A
31 fzonel ¬A0..^A
32 nelne2 x0..^A¬A0..^AxA
33 30 31 32 sylancl AWordXBXx0..^AxA
34 33 necomd AWordXBXx0..^AAx
35 fvunsn AxAABx=Ax
36 34 35 syl AWordXBXx0..^AAABx=Ax
37 29 36 eqtr4d AWordXBXx0..^AA++⟨“B”⟩x=AABx
38 fvexd AWordXBXAV
39 simpr AWordXBXBX
40 17 fdmd AWordXBXdomA=0..^A
41 40 eleq2d AWordXBXAdomAA0..^A
42 31 41 mtbiri AWordXBX¬AdomA
43 fsnunfv AVBX¬AdomAAABA=B
44 38 39 42 43 syl3anc AWordXBXAABA=B
45 simpl AWordXBXAWordX
46 s1cl BX⟨“B”⟩WordX
47 46 adantl AWordXBX⟨“B”⟩WordX
48 s1len ⟨“B”⟩=1
49 1nn 1
50 48 49 eqeltri ⟨“B”⟩
51 lbfzo0 00..^⟨“B”⟩⟨“B”⟩
52 50 51 mpbir 00..^⟨“B”⟩
53 52 a1i AWordXBX00..^⟨“B”⟩
54 ccatval3 AWordX⟨“B”⟩WordX00..^⟨“B”⟩A++⟨“B”⟩0+A=⟨“B”⟩0
55 45 47 53 54 syl3anc AWordXBXA++⟨“B”⟩0+A=⟨“B”⟩0
56 s1fv BX⟨“B”⟩0=B
57 56 adantl AWordXBX⟨“B”⟩0=B
58 55 57 eqtrd AWordXBXA++⟨“B”⟩0+A=B
59 6 adantr AWordXBXA0
60 59 nn0cnd AWordXBXA
61 60 addid2d AWordXBX0+A=A
62 61 fveq2d AWordXBXA++⟨“B”⟩0+A=A++⟨“B”⟩A
63 44 58 62 3eqtr2rd AWordXBXA++⟨“B”⟩A=AABA
64 elsni xAx=A
65 64 fveq2d xAA++⟨“B”⟩x=A++⟨“B”⟩A
66 64 fveq2d xAAABx=AABA
67 65 66 eqeq12d xAA++⟨“B”⟩x=AABxA++⟨“B”⟩A=AABA
68 63 67 syl5ibrcom AWordXBXxAA++⟨“B”⟩x=AABx
69 68 imp AWordXBXxAA++⟨“B”⟩x=AABx
70 37 69 jaodan AWordXBXx0..^AxAA++⟨“B”⟩x=AABx
71 27 70 sylan2b AWordXBXx0..^AAA++⟨“B”⟩x=AABx
72 15 26 71 eqfnfvd AWordXBXA++⟨“B”⟩=AAB