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

Theorem splval 13208
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 13014 . . 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 789 . . . . 5 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → 𝑠 = 𝑆)
4 fveq2 5986 . . . . . . . . 9 (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (1st𝑏) = (1st ‘⟨𝐹, 𝑇, 𝑅⟩))
54fveq2d 5990 . . . . . . . 8 (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (1st ‘(1st𝑏)) = (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
65adantl 480 . . . . . . 7 ((𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (1st ‘(1st𝑏)) = (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
7 ot1stg 6946 . . . . . . . 8 ((𝐹𝑊𝑇𝑋𝑅𝑌) → (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝐹)
87adantl 480 . . . . . . 7 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝐹)
96, 8sylan9eqr 2570 . . . . . 6 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (1st ‘(1st𝑏)) = 𝐹)
109opeq2d 4245 . . . . 5 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ⟨0, (1st ‘(1st𝑏))⟩ = ⟨0, 𝐹⟩)
113, 10oveq12d 6443 . . . 4 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) = (𝑆 substr ⟨0, 𝐹⟩))
12 fveq2 5986 . . . . . 6 (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (2nd𝑏) = (2nd ‘⟨𝐹, 𝑇, 𝑅⟩))
1312adantl 480 . . . . 5 ((𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd𝑏) = (2nd ‘⟨𝐹, 𝑇, 𝑅⟩))
14 ot3rdg 6948 . . . . . . 7 (𝑅𝑌 → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
15143ad2ant3 1076 . . . . . 6 ((𝐹𝑊𝑇𝑋𝑅𝑌) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
1615adantl 480 . . . . 5 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
1713, 16sylan9eqr 2570 . . . 4 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (2nd𝑏) = 𝑅)
1811, 17oveq12d 6443 . . 3 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) = ((𝑆 substr ⟨0, 𝐹⟩) ++ 𝑅))
194fveq2d 5990 . . . . . . 7 (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (2nd ‘(1st𝑏)) = (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
2019adantl 480 . . . . . 6 ((𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd ‘(1st𝑏)) = (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
21 ot2ndg 6947 . . . . . . 7 ((𝐹𝑊𝑇𝑋𝑅𝑌) → (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝑇)
2221adantl 480 . . . . . 6 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝑇)
2320, 22sylan9eqr 2570 . . . . 5 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (2nd ‘(1st𝑏)) = 𝑇)
243fveq2d 5990 . . . . 5 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (#‘𝑠) = (#‘𝑆))
2523, 24opeq12d 4246 . . . 4 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩ = ⟨𝑇, (#‘𝑆)⟩)
263, 25oveq12d 6443 . . 3 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (𝑠 substr ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩) = (𝑆 substr ⟨𝑇, (#‘𝑆)⟩))
2718, 26oveq12d 6443 . 2 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (((𝑠 substr ⟨0, (1st ‘(1st𝑏))⟩) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (#‘𝑠)⟩)) = (((𝑆 substr ⟨0, 𝐹⟩) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (#‘𝑆)⟩)))
28 elex 3089 . . 3 (𝑆𝑉𝑆 ∈ V)
2928adantr 479 . 2 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → 𝑆 ∈ V)
30 otex 4758 . . 3 𝐹, 𝑇, 𝑅⟩ ∈ V
3130a1i 11 . 2 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → ⟨𝐹, 𝑇, 𝑅⟩ ∈ V)
32 ovex 6453 . . 3 (((𝑆 substr ⟨0, 𝐹⟩) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (#‘𝑆)⟩)) ∈ V
3332a1i 11 . 2 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (((𝑆 substr ⟨0, 𝐹⟩) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (#‘𝑆)⟩)) ∈ V)
342, 27, 29, 31, 33ovmpt2d 6561 1 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 substr ⟨0, 𝐹⟩) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (#‘𝑆)⟩)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 382  w3a 1030   = wceq 1474  wcel 1938  Vcvv 3077  cop 4034  cotp 4036  cfv 5689  (class class class)co 6425  cmpt2 6427  1st c1st 6930  2nd c2nd 6931  0cc0 9689  #chash 12844   ++ cconcat 13003   substr csubstr 13005   splice csplice 13006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1700  ax-4 1713  ax-5 1793  ax-6 1838  ax-7 1885  ax-8 1940  ax-9 1947  ax-10 1966  ax-11 1971  ax-12 1983  ax-13 2137  ax-ext 2494  ax-sep 4607  ax-nul 4616  ax-pow 4668  ax-pr 4732  ax-un 6721
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1699  df-sb 1831  df-eu 2366  df-mo 2367  df-clab 2501  df-cleq 2507  df-clel 2510  df-nfc 2644  df-ral 2805  df-rex 2806  df-rab 2809  df-v 3079  df-sbc 3307  df-dif 3447  df-un 3449  df-in 3451  df-ss 3458  df-nul 3778  df-if 3940  df-sn 4029  df-pr 4031  df-op 4035  df-ot 4037  df-uni 4271  df-br 4482  df-opab 4542  df-mpt 4543  df-id 4847  df-xp 4938  df-rel 4939  df-cnv 4940  df-co 4941  df-dm 4942  df-rn 4943  df-iota 5653  df-fun 5691  df-fv 5697  df-ov 6428  df-oprab 6429  df-mpt2 6430  df-1st 6932  df-2nd 6933  df-splice 13014
This theorem is referenced by:  splid  13210  spllen  13211  splfv1  13212  splfv2a  13213  splval2  13214  gsumspl  17117  efgredleme  17908  efgredlemc  17910  efgcpbllemb  17920  frgpuplem  17937  splvalpfx  40208
  Copyright terms: Public domain W3C validator