Theorem splval 14928

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.

Step	Hyp	Ref	Expression
1		df-splice 14927	. . 3 ⊢ splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st ‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩)))
2	1	a1i 11	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → splice = (𝑠 ∈ V, 𝑏 ∈ V ↦ (((𝑠 prefix (1st ‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩))))
3		simprl 783	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → 𝑠 = 𝑆)
4		2fveq3 6913	. . . . . . 7 ⊢ (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (1st ‘(1st ‘𝑏)) = (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
5	4	adantl 487	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (1st ‘(1st ‘𝑏)) = (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
6		ot1stg 8039	. . . . . . 7 ⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝐹)
7	6	adantl 487	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝐹)
8	5, 7	sylan9eqr 2820	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (1st ‘(1st ‘𝑏)) = 𝐹)
9	3, 8	oveq12d 7461	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (𝑠 prefix (1st ‘(1st ‘𝑏))) = (𝑆 prefix 𝐹))
10		fveq2 6908	. . . . . 6 ⊢ (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (2nd ‘𝑏) = (2nd ‘⟨𝐹, 𝑇, 𝑅⟩))
11	10	adantl 487	. . . . 5 ⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd ‘𝑏) = (2nd ‘⟨𝐹, 𝑇, 𝑅⟩))
12		ot3rdg 8041	. . . . . . 7 ⊢ (𝑅 ∈ 𝑌 → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
13	12	3ad2ant3 1153	. . . . . 6 ⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
14	13	adantl 487	. . . . 5 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
15	11, 14	sylan9eqr 2820	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (2nd ‘𝑏) = 𝑅)
16	9, 15	oveq12d 7461	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ((𝑠 prefix (1st ‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) = ((𝑆 prefix 𝐹) ++ 𝑅))
17		2fveq3 6913	. . . . . . 7 ⊢ (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (2nd ‘(1st ‘𝑏)) = (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
18	17	adantl 487	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd ‘(1st ‘𝑏)) = (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
19		ot2ndg 8040	. . . . . . 7 ⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝑇)
20	19	adantl 487	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝑇)
21	18, 20	sylan9eqr 2820	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (2nd ‘(1st ‘𝑏)) = 𝑇)
22	3	fveq2d 6912	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (♯‘𝑠) = (♯‘𝑆))
23	21, 22	opeq12d 4851	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩ = ⟨𝑇, (♯‘𝑆)⟩)
24	3, 23	oveq12d 7461	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩) = (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))
25	16, 24	oveq12d 7461	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (((𝑠 prefix (1st ‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩)) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))
26		elex 3475	. . 3 ⊢ (𝑆 ∈ 𝑉 → 𝑆 ∈ V)
27	26	adantr 486	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → 𝑆 ∈ V)
28		otex 5438	. . 3 ⊢ ⟨𝐹, 𝑇, 𝑅⟩ ∈ V
29	28	a1i 11	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → ⟨𝐹, 𝑇, 𝑅⟩ ∈ V)
30		ovexd 7478	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)) ∈ V)
31	2, 25, 27, 29, 30	ovmpod 7596	1 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103   = wceq 1570   ∈ wcel 2147  Vcvv 3454  ⟨cop 4838  ⟨cotp 4861  ‘cfv 6558  (class class class)co 7443   ∈ cmpo 7445  1^st c1st 8023  2^nd c2nd 8024  ♯chash 14501   ++ cconcat 14742   substr csubstr 14816   prefix cpfx 14848   splice csplice 14926

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-sbc 3743  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-ot 4862  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-1st 8025  df-2nd 8026  df-splice 14927

This theorem is used by:  splid  14930  spllen  14931  splfv1  14932  splfv2a  14933  splval2  14934  gsumspl  19069  efgredleme  19987  efgredlemc  19989  efgcpbllemb  19999  frgpuplem  20016  splfv3  33589  cycpmco2f1  33755  cycpmco2rn  33756  cycpmco2lem2  33758  cycpmco2lem3  33759  cycpmco2lem4  33760  cycpmco2lem5  33761  cycpmco2lem6  33762  cycpmco2  33764