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

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

Proof of Theorem splval
Dummy variables 𝑠 𝑏 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-splice 14637 . . 3 splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st ‘(1st𝑏))) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)))
21a1i 11 . 2 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st ‘(1st𝑏))) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩))))
3 simprl 769 . . . . 5 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → 𝑠 = 𝑆)
4 2fveq3 6847 . . . . . . 7 (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (1st ‘(1st𝑏)) = (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
54adantl 482 . . . . . 6 ((𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (1st ‘(1st𝑏)) = (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
6 ot1stg 7934 . . . . . . 7 ((𝐹𝑊𝑇𝑋𝑅𝑌) → (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝐹)
76adantl 482 . . . . . 6 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝐹)
85, 7sylan9eqr 2798 . . . . 5 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (1st ‘(1st𝑏)) = 𝐹)
93, 8oveq12d 7374 . . . 4 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (𝑠 prefix (1st ‘(1st𝑏))) = (𝑆 prefix 𝐹))
10 fveq2 6842 . . . . . 6 (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (2nd𝑏) = (2nd ‘⟨𝐹, 𝑇, 𝑅⟩))
1110adantl 482 . . . . 5 ((𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd𝑏) = (2nd ‘⟨𝐹, 𝑇, 𝑅⟩))
12 ot3rdg 7936 . . . . . . 7 (𝑅𝑌 → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
13123ad2ant3 1135 . . . . . 6 ((𝐹𝑊𝑇𝑋𝑅𝑌) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
1413adantl 482 . . . . 5 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
1511, 14sylan9eqr 2798 . . . 4 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (2nd𝑏) = 𝑅)
169, 15oveq12d 7374 . . 3 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ((𝑠 prefix (1st ‘(1st𝑏))) ++ (2nd𝑏)) = ((𝑆 prefix 𝐹) ++ 𝑅))
17 2fveq3 6847 . . . . . . 7 (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (2nd ‘(1st𝑏)) = (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
1817adantl 482 . . . . . 6 ((𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd ‘(1st𝑏)) = (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
19 ot2ndg 7935 . . . . . . 7 ((𝐹𝑊𝑇𝑋𝑅𝑌) → (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝑇)
2019adantl 482 . . . . . 6 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝑇)
2118, 20sylan9eqr 2798 . . . . 5 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (2nd ‘(1st𝑏)) = 𝑇)
223fveq2d 6846 . . . . 5 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (♯‘𝑠) = (♯‘𝑆))
2321, 22opeq12d 4838 . . . 4 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩ = ⟨𝑇, (♯‘𝑆)⟩)
243, 23oveq12d 7374 . . 3 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩) = (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))
2516, 24oveq12d 7374 . 2 (((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) ∧ (𝑠 = 𝑆𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (((𝑠 prefix (1st ‘(1st𝑏))) ++ (2nd𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st𝑏)), (♯‘𝑠)⟩)) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))
26 elex 3463 . . 3 (𝑆𝑉𝑆 ∈ V)
2726adantr 481 . 2 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → 𝑆 ∈ V)
28 otex 5422 . . 3 𝐹, 𝑇, 𝑅⟩ ∈ V
2928a1i 11 . 2 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → ⟨𝐹, 𝑇, 𝑅⟩ ∈ V)
30 ovexd 7391 . 2 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)) ∈ V)
312, 25, 27, 29, 30ovmpod 7506 1 ((𝑆𝑉 ∧ (𝐹𝑊𝑇𝑋𝑅𝑌)) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  w3a 1087   = wceq 1541  wcel 2106  Vcvv 3445  cop 4592  cotp 4594  cfv 6496  (class class class)co 7356  cmpo 7358  1st c1st 7918  2nd c2nd 7919  chash 14229   ++ cconcat 14457   substr csubstr 14527   prefix cpfx 14557   splice csplice 14636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7671
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-sn 4587  df-pr 4589  df-op 4593  df-ot 4595  df-uni 4866  df-br 5106  df-opab 5168  df-mpt 5189  df-id 5531  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-iota 6448  df-fun 6498  df-fv 6504  df-ov 7359  df-oprab 7360  df-mpo 7361  df-1st 7920  df-2nd 7921  df-splice 14637
This theorem is referenced by:  splid  14640  spllen  14641  splfv1  14642  splfv2a  14643  splval2  14644  gsumspl  18653  efgredleme  19523  efgredlemc  19525  efgcpbllemb  19535  frgpuplem  19552  splfv3  31807  cycpmco2f1  31968  cycpmco2rn  31969  cycpmco2lem2  31971  cycpmco2lem3  31972  cycpmco2lem4  31973  cycpmco2lem5  31974  cycpmco2lem6  31975  cycpmco2  31977
  Copyright terms: Public domain W3C validator