MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  revccat Structured version   Visualization version   GIF version

Theorem revccat 14336
Description: Antiautomorphic property of the reversal operation. (Contributed by Stefan O'Rear, 27-Aug-2015.)
Assertion
Ref Expression
revccat ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) = ((reverse‘𝑇) ++ (reverse‘𝑆)))

Proof of Theorem revccat
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 ccatcl 14134 . . . 4 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (𝑆 ++ 𝑇) ∈ Word 𝐴)
2 revcl 14331 . . . 4 ((𝑆 ++ 𝑇) ∈ Word 𝐴 → (reverse‘(𝑆 ++ 𝑇)) ∈ Word 𝐴)
3 wrdfn 14088 . . . 4 ((reverse‘(𝑆 ++ 𝑇)) ∈ Word 𝐴 → (reverse‘(𝑆 ++ 𝑇)) Fn (0..^(♯‘(reverse‘(𝑆 ++ 𝑇)))))
41, 2, 33syl 18 . . 3 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) Fn (0..^(♯‘(reverse‘(𝑆 ++ 𝑇)))))
5 revlen 14332 . . . . . . 7 ((𝑆 ++ 𝑇) ∈ Word 𝐴 → (♯‘(reverse‘(𝑆 ++ 𝑇))) = (♯‘(𝑆 ++ 𝑇)))
61, 5syl 17 . . . . . 6 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (♯‘(reverse‘(𝑆 ++ 𝑇))) = (♯‘(𝑆 ++ 𝑇)))
7 ccatlen 14135 . . . . . 6 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑆) + (♯‘𝑇)))
8 lencl 14093 . . . . . . . 8 (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈ ℕ0)
98nn0cnd 12157 . . . . . . 7 (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈ ℂ)
10 lencl 14093 . . . . . . . 8 (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈ ℕ0)
1110nn0cnd 12157 . . . . . . 7 (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈ ℂ)
12 addcom 11023 . . . . . . 7 (((♯‘𝑆) ∈ ℂ ∧ (♯‘𝑇) ∈ ℂ) → ((♯‘𝑆) + (♯‘𝑇)) = ((♯‘𝑇) + (♯‘𝑆)))
139, 11, 12syl2an 599 . . . . . 6 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘𝑆) + (♯‘𝑇)) = ((♯‘𝑇) + (♯‘𝑆)))
146, 7, 133eqtrd 2781 . . . . 5 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (♯‘(reverse‘(𝑆 ++ 𝑇))) = ((♯‘𝑇) + (♯‘𝑆)))
1514oveq2d 7234 . . . 4 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (0..^(♯‘(reverse‘(𝑆 ++ 𝑇)))) = (0..^((♯‘𝑇) + (♯‘𝑆))))
1615fneq2d 6478 . . 3 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((reverse‘(𝑆 ++ 𝑇)) Fn (0..^(♯‘(reverse‘(𝑆 ++ 𝑇)))) ↔ (reverse‘(𝑆 ++ 𝑇)) Fn (0..^((♯‘𝑇) + (♯‘𝑆)))))
174, 16mpbid 235 . 2 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) Fn (0..^((♯‘𝑇) + (♯‘𝑆))))
18 revcl 14331 . . . . 5 (𝑇 ∈ Word 𝐴 → (reverse‘𝑇) ∈ Word 𝐴)
19 revcl 14331 . . . . 5 (𝑆 ∈ Word 𝐴 → (reverse‘𝑆) ∈ Word 𝐴)
20 ccatcl 14134 . . . . 5 (((reverse‘𝑇) ∈ Word 𝐴 ∧ (reverse‘𝑆) ∈ Word 𝐴) → ((reverse‘𝑇) ++ (reverse‘𝑆)) ∈ Word 𝐴)
2118, 19, 20syl2anr 600 . . . 4 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((reverse‘𝑇) ++ (reverse‘𝑆)) ∈ Word 𝐴)
22 wrdfn 14088 . . . 4 (((reverse‘𝑇) ++ (reverse‘𝑆)) ∈ Word 𝐴 → ((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^(♯‘((reverse‘𝑇) ++ (reverse‘𝑆)))))
2321, 22syl 17 . . 3 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^(♯‘((reverse‘𝑇) ++ (reverse‘𝑆)))))
24 ccatlen 14135 . . . . . . 7 (((reverse‘𝑇) ∈ Word 𝐴 ∧ (reverse‘𝑆) ∈ Word 𝐴) → (♯‘((reverse‘𝑇) ++ (reverse‘𝑆))) = ((♯‘(reverse‘𝑇)) + (♯‘(reverse‘𝑆))))
2518, 19, 24syl2anr 600 . . . . . 6 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (♯‘((reverse‘𝑇) ++ (reverse‘𝑆))) = ((♯‘(reverse‘𝑇)) + (♯‘(reverse‘𝑆))))
26 revlen 14332 . . . . . . 7 (𝑇 ∈ Word 𝐴 → (♯‘(reverse‘𝑇)) = (♯‘𝑇))
27 revlen 14332 . . . . . . 7 (𝑆 ∈ Word 𝐴 → (♯‘(reverse‘𝑆)) = (♯‘𝑆))
2826, 27oveqan12rd 7238 . . . . . 6 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘(reverse‘𝑇)) + (♯‘(reverse‘𝑆))) = ((♯‘𝑇) + (♯‘𝑆)))
2925, 28eqtrd 2777 . . . . 5 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (♯‘((reverse‘𝑇) ++ (reverse‘𝑆))) = ((♯‘𝑇) + (♯‘𝑆)))
3029oveq2d 7234 . . . 4 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (0..^(♯‘((reverse‘𝑇) ++ (reverse‘𝑆)))) = (0..^((♯‘𝑇) + (♯‘𝑆))))
3130fneq2d 6478 . . 3 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^(♯‘((reverse‘𝑇) ++ (reverse‘𝑆)))) ↔ ((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^((♯‘𝑇) + (♯‘𝑆)))))
3223, 31mpbid 235 . 2 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((reverse‘𝑇) ++ (reverse‘𝑆)) Fn (0..^((♯‘𝑇) + (♯‘𝑆))))
33 id 22 . . . 4 (𝑥 ∈ (0..^((♯‘𝑇) + (♯‘𝑆))) → 𝑥 ∈ (0..^((♯‘𝑇) + (♯‘𝑆))))
3410nn0zd 12285 . . . . 5 (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈ ℤ)
3534adantl 485 . . . 4 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (♯‘𝑇) ∈ ℤ)
36 fzospliti 13279 . . . 4 ((𝑥 ∈ (0..^((♯‘𝑇) + (♯‘𝑆))) ∧ (♯‘𝑇) ∈ ℤ) → (𝑥 ∈ (0..^(♯‘𝑇)) ∨ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))))
3733, 35, 36syl2anr 600 . . 3 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑥 ∈ (0..^(♯‘𝑇)) ∨ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))))
38 simpll 767 . . . . . . 7 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑆 ∈ Word 𝐴)
39 simplr 769 . . . . . . 7 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑇 ∈ Word 𝐴)
40 fzoval 13249 . . . . . . . . . . . . 13 ((♯‘𝑇) ∈ ℤ → (0..^(♯‘𝑇)) = (0...((♯‘𝑇) − 1)))
4134, 40syl 17 . . . . . . . . . . . 12 (𝑇 ∈ Word 𝐴 → (0..^(♯‘𝑇)) = (0...((♯‘𝑇) − 1)))
4241adantl 485 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (0..^(♯‘𝑇)) = (0...((♯‘𝑇) − 1)))
4342eleq2d 2823 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (𝑥 ∈ (0..^(♯‘𝑇)) ↔ 𝑥 ∈ (0...((♯‘𝑇) − 1))))
4443biimpa 480 . . . . . . . . 9 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0...((♯‘𝑇) − 1)))
45 fznn0sub2 13224 . . . . . . . . 9 (𝑥 ∈ (0...((♯‘𝑇) − 1)) → (((♯‘𝑇) − 1) − 𝑥) ∈ (0...((♯‘𝑇) − 1)))
4644, 45syl 17 . . . . . . . 8 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((♯‘𝑇) − 1) − 𝑥) ∈ (0...((♯‘𝑇) − 1)))
4741ad2antlr 727 . . . . . . . 8 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (0..^(♯‘𝑇)) = (0...((♯‘𝑇) − 1)))
4846, 47eleqtrrd 2841 . . . . . . 7 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((♯‘𝑇) − 1) − 𝑥) ∈ (0..^(♯‘𝑇)))
49 ccatval3 14141 . . . . . . 7 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴 ∧ (((♯‘𝑇) − 1) − 𝑥) ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆))) = (𝑇‘(((♯‘𝑇) − 1) − 𝑥)))
5038, 39, 48, 49syl3anc 1373 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆))) = (𝑇‘(((♯‘𝑇) − 1) − 𝑥)))
517, 13eqtrd 2777 . . . . . . . . . . . 12 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (♯‘(𝑆 ++ 𝑇)) = ((♯‘𝑇) + (♯‘𝑆)))
5251oveq1d 7233 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘(𝑆 ++ 𝑇)) − 1) = (((♯‘𝑇) + (♯‘𝑆)) − 1))
5311adantl 485 . . . . . . . . . . . 12 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (♯‘𝑇) ∈ ℂ)
549adantr 484 . . . . . . . . . . . 12 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (♯‘𝑆) ∈ ℂ)
55 1cnd 10833 . . . . . . . . . . . 12 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → 1 ∈ ℂ)
5653, 54, 55addsubd 11215 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (((♯‘𝑇) + (♯‘𝑆)) − 1) = (((♯‘𝑇) − 1) + (♯‘𝑆)))
5752, 56eqtrd 2777 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘(𝑆 ++ 𝑇)) − 1) = (((♯‘𝑇) − 1) + (♯‘𝑆)))
5857oveq1d 7233 . . . . . . . . 9 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) − 1) + (♯‘𝑆)) − 𝑥))
5958adantr 484 . . . . . . . 8 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) − 1) + (♯‘𝑆)) − 𝑥))
60 peano2zm 12225 . . . . . . . . . . . 12 ((♯‘𝑇) ∈ ℤ → ((♯‘𝑇) − 1) ∈ ℤ)
6134, 60syl 17 . . . . . . . . . . 11 (𝑇 ∈ Word 𝐴 → ((♯‘𝑇) − 1) ∈ ℤ)
6261zcnd 12288 . . . . . . . . . 10 (𝑇 ∈ Word 𝐴 → ((♯‘𝑇) − 1) ∈ ℂ)
6362ad2antlr 727 . . . . . . . . 9 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((♯‘𝑇) − 1) ∈ ℂ)
649ad2antrr 726 . . . . . . . . 9 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (♯‘𝑆) ∈ ℂ)
65 elfzoelz 13248 . . . . . . . . . . 11 (𝑥 ∈ (0..^(♯‘𝑇)) → 𝑥 ∈ ℤ)
6665zcnd 12288 . . . . . . . . . 10 (𝑥 ∈ (0..^(♯‘𝑇)) → 𝑥 ∈ ℂ)
6766adantl 485 . . . . . . . . 9 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ ℂ)
6863, 64, 67addsubd 11215 . . . . . . . 8 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((((♯‘𝑇) − 1) + (♯‘𝑆)) − 𝑥) = ((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆)))
6959, 68eqtrd 2777 . . . . . . 7 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆)))
7069fveq2d 6726 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = ((𝑆 ++ 𝑇)‘((((♯‘𝑇) − 1) − 𝑥) + (♯‘𝑆))))
71 revfv 14333 . . . . . . 7 ((𝑇 ∈ Word 𝐴𝑥 ∈ (0..^(♯‘𝑇))) → ((reverse‘𝑇)‘𝑥) = (𝑇‘(((♯‘𝑇) − 1) − 𝑥)))
7271adantll 714 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((reverse‘𝑇)‘𝑥) = (𝑇‘(((♯‘𝑇) − 1) − 𝑥)))
7350, 70, 723eqtr4d 2787 . . . . 5 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = ((reverse‘𝑇)‘𝑥))
7434uzidd 12459 . . . . . . . . . 10 (𝑇 ∈ Word 𝐴 → (♯‘𝑇) ∈ (ℤ‘(♯‘𝑇)))
75 uzaddcl 12505 . . . . . . . . . 10 (((♯‘𝑇) ∈ (ℤ‘(♯‘𝑇)) ∧ (♯‘𝑆) ∈ ℕ0) → ((♯‘𝑇) + (♯‘𝑆)) ∈ (ℤ‘(♯‘𝑇)))
7674, 8, 75syl2anr 600 . . . . . . . . 9 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘𝑇) + (♯‘𝑆)) ∈ (ℤ‘(♯‘𝑇)))
7751, 76eqeltrd 2838 . . . . . . . 8 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (♯‘(𝑆 ++ 𝑇)) ∈ (ℤ‘(♯‘𝑇)))
78 fzoss2 13275 . . . . . . . 8 ((♯‘(𝑆 ++ 𝑇)) ∈ (ℤ‘(♯‘𝑇)) → (0..^(♯‘𝑇)) ⊆ (0..^(♯‘(𝑆 ++ 𝑇))))
7977, 78syl 17 . . . . . . 7 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (0..^(♯‘𝑇)) ⊆ (0..^(♯‘(𝑆 ++ 𝑇))))
8079sselda 3906 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^(♯‘(𝑆 ++ 𝑇))))
81 revfv 14333 . . . . . 6 (((𝑆 ++ 𝑇) ∈ Word 𝐴𝑥 ∈ (0..^(♯‘(𝑆 ++ 𝑇)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)))
821, 80, 81syl2an2r 685 . . . . 5 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)))
8318ad2antlr 727 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (reverse‘𝑇) ∈ Word 𝐴)
8419ad2antrr 726 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (reverse‘𝑆) ∈ Word 𝐴)
8526adantl 485 . . . . . . . . 9 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (♯‘(reverse‘𝑇)) = (♯‘𝑇))
8685oveq2d 7234 . . . . . . . 8 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (0..^(♯‘(reverse‘𝑇))) = (0..^(♯‘𝑇)))
8786eleq2d 2823 . . . . . . 7 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (𝑥 ∈ (0..^(♯‘(reverse‘𝑇))) ↔ 𝑥 ∈ (0..^(♯‘𝑇))))
8887biimpar 481 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → 𝑥 ∈ (0..^(♯‘(reverse‘𝑇))))
89 ccatval1 14138 . . . . . 6 (((reverse‘𝑇) ∈ Word 𝐴 ∧ (reverse‘𝑆) ∈ Word 𝐴𝑥 ∈ (0..^(♯‘(reverse‘𝑇)))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑇)‘𝑥))
9083, 84, 88, 89syl3anc 1373 . . . . 5 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑇)‘𝑥))
9173, 82, 903eqtr4d 2787 . . . 4 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^(♯‘𝑇))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥))
928nn0zd 12285 . . . . . . . . . . . 12 (𝑆 ∈ Word 𝐴 → (♯‘𝑆) ∈ ℤ)
93 peano2zm 12225 . . . . . . . . . . . 12 ((♯‘𝑆) ∈ ℤ → ((♯‘𝑆) − 1) ∈ ℤ)
9492, 93syl 17 . . . . . . . . . . 11 (𝑆 ∈ Word 𝐴 → ((♯‘𝑆) − 1) ∈ ℤ)
9594zcnd 12288 . . . . . . . . . 10 (𝑆 ∈ Word 𝐴 → ((♯‘𝑆) − 1) ∈ ℂ)
9695ad2antrr 726 . . . . . . . . 9 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((♯‘𝑆) − 1) ∈ ℂ)
97 elfzoelz 13248 . . . . . . . . . . 11 (𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) → 𝑥 ∈ ℤ)
9897zcnd 12288 . . . . . . . . . 10 (𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) → 𝑥 ∈ ℂ)
9998adantl 485 . . . . . . . . 9 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑥 ∈ ℂ)
10011ad2antlr 727 . . . . . . . . 9 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (♯‘𝑇) ∈ ℂ)
10196, 99, 100subsub3d 11224 . . . . . . . 8 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘𝑆) − 1) − (𝑥 − (♯‘𝑇))) = ((((♯‘𝑆) − 1) + (♯‘𝑇)) − 𝑥))
10226oveq2d 7234 . . . . . . . . . 10 (𝑇 ∈ Word 𝐴 → (𝑥 − (♯‘(reverse‘𝑇))) = (𝑥 − (♯‘𝑇)))
103102oveq2d 7234 . . . . . . . . 9 (𝑇 ∈ Word 𝐴 → (((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇)))) = (((♯‘𝑆) − 1) − (𝑥 − (♯‘𝑇))))
104103ad2antlr 727 . . . . . . . 8 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇)))) = (((♯‘𝑆) − 1) − (𝑥 − (♯‘𝑇))))
1057oveq1d 7233 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘(𝑆 ++ 𝑇)) − 1) = (((♯‘𝑆) + (♯‘𝑇)) − 1))
10654, 53, 55addsubd 11215 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (((♯‘𝑆) + (♯‘𝑇)) − 1) = (((♯‘𝑆) − 1) + (♯‘𝑇)))
107105, 106eqtrd 2777 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘(𝑆 ++ 𝑇)) − 1) = (((♯‘𝑆) − 1) + (♯‘𝑇)))
108107oveq1d 7233 . . . . . . . . 9 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑆) − 1) + (♯‘𝑇)) − 𝑥))
109108adantr 484 . . . . . . . 8 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑆) − 1) + (♯‘𝑇)) − 𝑥))
110101, 104, 1093eqtr4rd 2788 . . . . . . 7 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = (((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇)))))
111110fveq2d 6726 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑆‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = (𝑆‘(((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇))))))
112 simpll 767 . . . . . . 7 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑆 ∈ Word 𝐴)
113 simplr 769 . . . . . . 7 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑇 ∈ Word 𝐴)
114 zaddcl 12222 . . . . . . . . . . 11 (((♯‘𝑇) ∈ ℤ ∧ (♯‘𝑆) ∈ ℤ) → ((♯‘𝑇) + (♯‘𝑆)) ∈ ℤ)
11534, 92, 114syl2anr 600 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘𝑇) + (♯‘𝑆)) ∈ ℤ)
116 peano2zm 12225 . . . . . . . . . 10 (((♯‘𝑇) + (♯‘𝑆)) ∈ ℤ → (((♯‘𝑇) + (♯‘𝑆)) − 1) ∈ ℤ)
117115, 116syl 17 . . . . . . . . 9 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (((♯‘𝑇) + (♯‘𝑆)) − 1) ∈ ℤ)
118 fzoval 13249 . . . . . . . . . . . 12 (((♯‘𝑇) + (♯‘𝑆)) ∈ ℤ → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) = ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1)))
119115, 118syl 17 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) = ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1)))
120119eleq2d 2823 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ↔ 𝑥 ∈ ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1))))
121120biimpa 480 . . . . . . . . 9 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑥 ∈ ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1)))
122 fzrev2i 13182 . . . . . . . . 9 (((((♯‘𝑇) + (♯‘𝑆)) − 1) ∈ ℤ ∧ 𝑥 ∈ ((♯‘𝑇)...(((♯‘𝑇) + (♯‘𝑆)) − 1))) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − 𝑥) ∈ (((((♯‘𝑇) + (♯‘𝑆)) − 1) − (((♯‘𝑇) + (♯‘𝑆)) − 1))...((((♯‘𝑇) + (♯‘𝑆)) − 1) − (♯‘𝑇))))
123117, 121, 122syl2an2r 685 . . . . . . . 8 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − 𝑥) ∈ (((((♯‘𝑇) + (♯‘𝑆)) − 1) − (((♯‘𝑇) + (♯‘𝑆)) − 1))...((((♯‘𝑇) + (♯‘𝑆)) − 1) − (♯‘𝑇))))
12452oveq1d 7233 . . . . . . . . 9 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) + (♯‘𝑆)) − 1) − 𝑥))
125124adantr 484 . . . . . . . 8 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) = ((((♯‘𝑇) + (♯‘𝑆)) − 1) − 𝑥))
12692adantr 484 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (♯‘𝑆) ∈ ℤ)
127 fzoval 13249 . . . . . . . . . . 11 ((♯‘𝑆) ∈ ℤ → (0..^(♯‘𝑆)) = (0...((♯‘𝑆) − 1)))
128126, 127syl 17 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (0..^(♯‘𝑆)) = (0...((♯‘𝑆) − 1)))
129117zcnd 12288 . . . . . . . . . . . 12 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (((♯‘𝑇) + (♯‘𝑆)) − 1) ∈ ℂ)
130129subidd 11182 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − (((♯‘𝑇) + (♯‘𝑆)) − 1)) = 0)
131 addcl 10816 . . . . . . . . . . . . . 14 (((♯‘𝑇) ∈ ℂ ∧ (♯‘𝑆) ∈ ℂ) → ((♯‘𝑇) + (♯‘𝑆)) ∈ ℂ)
13211, 9, 131syl2anr 600 . . . . . . . . . . . . 13 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘𝑇) + (♯‘𝑆)) ∈ ℂ)
133132, 55, 53sub32d 11226 . . . . . . . . . . . 12 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − (♯‘𝑇)) = ((((♯‘𝑇) + (♯‘𝑆)) − (♯‘𝑇)) − 1))
134 pncan2 11090 . . . . . . . . . . . . . 14 (((♯‘𝑇) ∈ ℂ ∧ (♯‘𝑆) ∈ ℂ) → (((♯‘𝑇) + (♯‘𝑆)) − (♯‘𝑇)) = (♯‘𝑆))
13511, 9, 134syl2anr 600 . . . . . . . . . . . . 13 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (((♯‘𝑇) + (♯‘𝑆)) − (♯‘𝑇)) = (♯‘𝑆))
136135oveq1d 7233 . . . . . . . . . . . 12 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((((♯‘𝑇) + (♯‘𝑆)) − (♯‘𝑇)) − 1) = ((♯‘𝑆) − 1))
137133, 136eqtrd 2777 . . . . . . . . . . 11 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((((♯‘𝑇) + (♯‘𝑆)) − 1) − (♯‘𝑇)) = ((♯‘𝑆) − 1))
138130, 137oveq12d 7236 . . . . . . . . . 10 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (((((♯‘𝑇) + (♯‘𝑆)) − 1) − (((♯‘𝑇) + (♯‘𝑆)) − 1))...((((♯‘𝑇) + (♯‘𝑆)) − 1) − (♯‘𝑇))) = (0...((♯‘𝑆) − 1)))
139128, 138eqtr4d 2780 . . . . . . . . 9 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (0..^(♯‘𝑆)) = (((((♯‘𝑇) + (♯‘𝑆)) − 1) − (((♯‘𝑇) + (♯‘𝑆)) − 1))...((((♯‘𝑇) + (♯‘𝑆)) − 1) − (♯‘𝑇))))
140139adantr 484 . . . . . . . 8 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (0..^(♯‘𝑆)) = (((((♯‘𝑇) + (♯‘𝑆)) − 1) − (((♯‘𝑇) + (♯‘𝑆)) − 1))...((((♯‘𝑇) + (♯‘𝑆)) − 1) − (♯‘𝑇))))
141123, 125, 1403eltr4d 2853 . . . . . . 7 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) ∈ (0..^(♯‘𝑆)))
142 ccatval1 14138 . . . . . . 7 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴 ∧ (((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥) ∈ (0..^(♯‘𝑆))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = (𝑆‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)))
143112, 113, 141, 142syl3anc 1373 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = (𝑆‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)))
144 simpl 486 . . . . . . 7 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → 𝑆 ∈ Word 𝐴)
145102ad2antlr 727 . . . . . . . 8 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑥 − (♯‘(reverse‘𝑇))) = (𝑥 − (♯‘𝑇)))
146 id 22 . . . . . . . . 9 (𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) → 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))))
147 fzosubel3 13308 . . . . . . . . 9 ((𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ∧ (♯‘𝑆) ∈ ℤ) → (𝑥 − (♯‘𝑇)) ∈ (0..^(♯‘𝑆)))
148146, 126, 147syl2anr 600 . . . . . . . 8 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑥 − (♯‘𝑇)) ∈ (0..^(♯‘𝑆)))
149145, 148eqeltrd 2838 . . . . . . 7 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (𝑥 − (♯‘(reverse‘𝑇))) ∈ (0..^(♯‘𝑆)))
150 revfv 14333 . . . . . . 7 ((𝑆 ∈ Word 𝐴 ∧ (𝑥 − (♯‘(reverse‘𝑇))) ∈ (0..^(♯‘𝑆))) → ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇)))) = (𝑆‘(((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇))))))
151144, 149, 150syl2an2r 685 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇)))) = (𝑆‘(((♯‘𝑆) − 1) − (𝑥 − (♯‘(reverse‘𝑇))))))
152111, 143, 1513eqtr4d 2787 . . . . 5 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)) = ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇)))))
153 fzoss1 13274 . . . . . . . . . . 11 ((♯‘𝑇) ∈ (ℤ‘0) → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆ (0..^((♯‘𝑇) + (♯‘𝑆))))
154 nn0uz 12481 . . . . . . . . . . 11 0 = (ℤ‘0)
155153, 154eleq2s 2856 . . . . . . . . . 10 ((♯‘𝑇) ∈ ℕ0 → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆ (0..^((♯‘𝑇) + (♯‘𝑆))))
15610, 155syl 17 . . . . . . . . 9 (𝑇 ∈ Word 𝐴 → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆ (0..^((♯‘𝑇) + (♯‘𝑆))))
157156adantl 485 . . . . . . . 8 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆ (0..^((♯‘𝑇) + (♯‘𝑆))))
15851oveq2d 7234 . . . . . . . 8 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (0..^(♯‘(𝑆 ++ 𝑇))) = (0..^((♯‘𝑇) + (♯‘𝑆))))
159157, 158sseqtrrd 3947 . . . . . . 7 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))) ⊆ (0..^(♯‘(𝑆 ++ 𝑇))))
160159sselda 3906 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑥 ∈ (0..^(♯‘(𝑆 ++ 𝑇))))
1611, 160, 81syl2an2r 685 . . . . 5 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = ((𝑆 ++ 𝑇)‘(((♯‘(𝑆 ++ 𝑇)) − 1) − 𝑥)))
16218ad2antlr 727 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (reverse‘𝑇) ∈ Word 𝐴)
16319ad2antrr 726 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (reverse‘𝑆) ∈ Word 𝐴)
16485, 28oveq12d 7236 . . . . . . . 8 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → ((♯‘(reverse‘𝑇))..^((♯‘(reverse‘𝑇)) + (♯‘(reverse‘𝑆)))) = ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))))
165164eleq2d 2823 . . . . . . 7 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (𝑥 ∈ ((♯‘(reverse‘𝑇))..^((♯‘(reverse‘𝑇)) + (♯‘(reverse‘𝑆)))) ↔ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))))
166165biimpar 481 . . . . . 6 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → 𝑥 ∈ ((♯‘(reverse‘𝑇))..^((♯‘(reverse‘𝑇)) + (♯‘(reverse‘𝑆)))))
167 ccatval2 14140 . . . . . 6 (((reverse‘𝑇) ∈ Word 𝐴 ∧ (reverse‘𝑆) ∈ Word 𝐴𝑥 ∈ ((♯‘(reverse‘𝑇))..^((♯‘(reverse‘𝑇)) + (♯‘(reverse‘𝑆))))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇)))))
168162, 163, 166, 167syl3anc 1373 . . . . 5 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥) = ((reverse‘𝑆)‘(𝑥 − (♯‘(reverse‘𝑇)))))
169152, 161, 1683eqtr4d 2787 . . . 4 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥))
17091, 169jaodan 958 . . 3 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ (𝑥 ∈ (0..^(♯‘𝑇)) ∨ 𝑥 ∈ ((♯‘𝑇)..^((♯‘𝑇) + (♯‘𝑆))))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥))
17137, 170syldan 594 . 2 (((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) ∧ 𝑥 ∈ (0..^((♯‘𝑇) + (♯‘𝑆)))) → ((reverse‘(𝑆 ++ 𝑇))‘𝑥) = (((reverse‘𝑇) ++ (reverse‘𝑆))‘𝑥))
17217, 32, 171eqfnfvd 6860 1 ((𝑆 ∈ Word 𝐴𝑇 ∈ Word 𝐴) → (reverse‘(𝑆 ++ 𝑇)) = ((reverse‘𝑇) ++ (reverse‘𝑆)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 399  wo 847   = wceq 1543  wcel 2110  wss 3871   Fn wfn 6380  cfv 6385  (class class class)co 7218  cc 10732  0cc0 10734  1c1 10735   + caddc 10737  cmin 11067  0cn0 12095  cz 12181  cuz 12443  ...cfz 13100  ..^cfzo 13243  chash 13901  Word cword 14074   ++ cconcat 14130  reversecreverse 14328
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-10 2141  ax-11 2158  ax-12 2175  ax-ext 2708  ax-rep 5184  ax-sep 5197  ax-nul 5204  ax-pow 5263  ax-pr 5327  ax-un 7528  ax-cnex 10790  ax-resscn 10791  ax-1cn 10792  ax-icn 10793  ax-addcl 10794  ax-addrcl 10795  ax-mulcl 10796  ax-mulrcl 10797  ax-mulcom 10798  ax-addass 10799  ax-mulass 10800  ax-distr 10801  ax-i2m1 10802  ax-1ne0 10803  ax-1rid 10804  ax-rnegex 10805  ax-rrecex 10806  ax-cnre 10807  ax-pre-lttri 10808  ax-pre-lttrn 10809  ax-pre-ltadd 10810  ax-pre-mulgt0 10811
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2071  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2886  df-ne 2941  df-nel 3047  df-ral 3066  df-rex 3067  df-reu 3068  df-rab 3070  df-v 3415  df-sbc 3700  df-csb 3817  df-dif 3874  df-un 3876  df-in 3878  df-ss 3888  df-pss 3890  df-nul 4243  df-if 4445  df-pw 4520  df-sn 4547  df-pr 4549  df-tp 4551  df-op 4553  df-uni 4825  df-int 4865  df-iun 4911  df-br 5059  df-opab 5121  df-mpt 5141  df-tr 5167  df-id 5460  df-eprel 5465  df-po 5473  df-so 5474  df-fr 5514  df-we 5516  df-xp 5562  df-rel 5563  df-cnv 5564  df-co 5565  df-dm 5566  df-rn 5567  df-res 5568  df-ima 5569  df-pred 6165  df-ord 6221  df-on 6222  df-lim 6223  df-suc 6224  df-iota 6343  df-fun 6387  df-fn 6388  df-f 6389  df-f1 6390  df-fo 6391  df-f1o 6392  df-fv 6393  df-riota 7175  df-ov 7221  df-oprab 7222  df-mpo 7223  df-om 7650  df-1st 7766  df-2nd 7767  df-wrecs 8052  df-recs 8113  df-rdg 8151  df-1o 8207  df-er 8396  df-en 8632  df-dom 8633  df-sdom 8634  df-fin 8635  df-card 9560  df-pnf 10874  df-mnf 10875  df-xr 10876  df-ltxr 10877  df-le 10878  df-sub 11069  df-neg 11070  df-nn 11836  df-n0 12096  df-z 12182  df-uz 12444  df-fz 13101  df-fzo 13244  df-hash 13902  df-word 14075  df-concat 14131  df-reverse 14329
This theorem is referenced by:  gsumwrev  18763  efginvrel2  19122
  Copyright terms: Public domain W3C validator