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

Theorem splval 13702
Description: Value of the substring replacement operator. (Contributed by Stefan O'Rear, 15-Aug-2015.)
Assertion
Ref Expression
splval ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 substr ⟨0, 𝐹⟩) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))

Proof of Theorem splval
Dummy variables 𝑠 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-splice 13490 . . 3 splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)))
21a1i 11 . 2 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩))))
3 simprl 811 . . . . 5 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → 𝑠 = 𝑆)
4 fveq2 6352 . . . . . . . . 9 (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (1st𝑏) = (1st ‘⟨𝐹, 𝑇, 𝑅⟩))
54fveq2d 6356 . . . . . . . 8 (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (1st ‘(1st𝑏)) = (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
65adantl 473 . . . . . . 7 ((𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (1st ‘(1st𝑏)) = (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
7 ot1stg 7347 . . . . . . . 8 ((𝐹𝑊𝑇𝑋𝑅𝑌) → (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝐹)
87adantl 473 . . . . . . 7 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝐹)
96, 8sylan9eqr 2816 . . . . . 6 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (1st ‘(1st𝑏)) = 𝐹)
109opeq2d 4560 . . . . 5 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ⟨0, (1st ‘(1st𝑏))⟩ = ⟨0, 𝐹⟩)
113, 10oveq12d 6831 . . . 4 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) = (𝑆 substr ⟨0, 𝐹⟩))
12 fveq2 6352 . . . . . 6 (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (2nd𝑏) = (2nd ‘⟨𝐹, 𝑇, 𝑅⟩))
1312adantl 473 . . . . 5 ((𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd𝑏) = (2nd ‘⟨𝐹, 𝑇, 𝑅⟩))
14 ot3rdg 7349 . . . . . . 7 (𝑅𝑌 → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
15143ad2ant3 1130 . . . . . 6 ((𝐹𝑊𝑇𝑋𝑅𝑌) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
1615adantl 473 . . . . 5 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
1713, 16sylan9eqr 2816 . . . 4 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (2nd𝑏) = 𝑅)
1811, 17oveq12d 6831 . . 3 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) = ((𝑆 substr ⟨0, 𝐹⟩) ++ 𝑅))
194fveq2d 6356 . . . . . . 7 (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (2nd ‘(1st𝑏)) = (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
2019adantl 473 . . . . . 6 ((𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd ‘(1st𝑏)) = (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
21 ot2ndg 7348 . . . . . . 7 ((𝐹𝑊𝑇𝑋𝑅𝑌) → (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝑇)
2221adantl 473 . . . . . 6 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝑇)
2320, 22sylan9eqr 2816 . . . . 5 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (2nd ‘(1st𝑏)) = 𝑇)
243fveq2d 6356 . . . . 5 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (♯‘𝑠) = (♯‘𝑆))
2523, 24opeq12d 4561 . . . 4 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩ = ⟨𝑇, (♯‘𝑆)⟩)
263, 25oveq12d 6831 . . 3 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩) = (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))
2718, 26oveq12d 6831 . 2 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)) = (((𝑆 substr ⟨0, 𝐹⟩) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))
28 elex 3352 . . 3 (𝑆𝑉𝑆 ∈ V)
2928adantr 472 . 2 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → 𝑆 ∈ V)
30 otex 5082 . . 3 𝐹, 𝑇, 𝑅⟩ ∈ V
3130a1i 11 . 2 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → ⟨𝐹, 𝑇, 𝑅⟩ ∈ V)
32 ovexd 6843 . 2 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (((𝑆 substr ⟨0, 𝐹⟩) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)) ∈ V)
332, 27, 29, 31, 32ovmpt2d 6953 1 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 substr ⟨0, 𝐹⟩) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3a 1072   = wceq 1632  wcel 2139  Vcvv 3340  cop 4327  cotp 4329  cfv 6049  (class class class)co 6813  cmpt2 6815  1st c1st 7331  2nd c2nd 7332  0cc0 10128  chash 13311   ++ cconcat 13479   substr csubstr 13481   splice csplice 13482
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-8 2141  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-sep 4933  ax-nul 4941  ax-pow 4992  ax-pr 5055  ax-un 7114
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-mo 2612  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-ot 4330  df-uni 4589  df-br 4805  df-opab 4865  df-mpt 4882  df-id 5174  df-xp 5272  df-rel 5273  df-cnv 5274  df-co 5275  df-dm 5276  df-rn 5277  df-iota 6012  df-fun 6051  df-fv 6057  df-ov 6816  df-oprab 6817  df-mpt2 6818  df-1st 7333  df-2nd 7334  df-splice 13490
This theorem is referenced by:  splid  13704  spllen  13705  splfv1  13706  splfv2a  13707  splval2  13708  gsumspl  17582  efgredleme  18356  efgredlemc  18358  efgcpbllemb  18368  frgpuplem  18385  splvalpfx  41945
  Copyright terms: Public domain W3C validator