Theorem splval 14711

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 14710	. . 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 776	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → 𝑠 = 𝑆)
4		2fveq3 6839	. . . . . . 7 ⊢ (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (1st ‘(1st ‘𝑏)) = (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
5	4	adantl 482	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (1st ‘(1st ‘𝑏)) = (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
6		ot1stg 7952	. . . . . . 7 ⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝐹)
7	6	adantl 482	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (1st ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝐹)
8	5, 7	sylan9eqr 2797	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (1st ‘(1st ‘𝑏)) = 𝐹)
9	3, 8	oveq12d 7381	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (𝑠 prefix (1st ‘(1st ‘𝑏))) = (𝑆 prefix 𝐹))
10		fveq2 6834	. . . . . 6 ⊢ (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (2nd ‘𝑏) = (2nd ‘⟨𝐹, 𝑇, 𝑅⟩))
11	10	adantl 482	. . . . 5 ⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd ‘𝑏) = (2nd ‘⟨𝐹, 𝑇, 𝑅⟩))
12		ot3rdg 7954	. . . . . . 7 ⊢ (𝑅 ∈ 𝑌 → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
13	12	3ad2ant3 1141	. . . . . 6 ⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
14	13	adantl 482	. . . . 5 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (2nd ‘⟨𝐹, 𝑇, 𝑅⟩) = 𝑅)
15	11, 14	sylan9eqr 2797	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (2nd ‘𝑏) = 𝑅)
16	9, 15	oveq12d 7381	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ((𝑠 prefix (1st ‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) = ((𝑆 prefix 𝐹) ++ 𝑅))
17		2fveq3 6839	. . . . . . 7 ⊢ (𝑏 = ⟨𝐹, 𝑇, 𝑅⟩ → (2nd ‘(1st ‘𝑏)) = (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
18	17	adantl 482	. . . . . 6 ⊢ ((𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩) → (2nd ‘(1st ‘𝑏)) = (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)))
19		ot2ndg 7953	. . . . . . 7 ⊢ ((𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) → (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝑇)
20	19	adantl 482	. . . . . 6 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (2nd ‘(1st ‘⟨𝐹, 𝑇, 𝑅⟩)) = 𝑇)
21	18, 20	sylan9eqr 2797	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (2nd ‘(1st ‘𝑏)) = 𝑇)
22	3	fveq2d 6838	. . . . 5 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (♯‘𝑠) = (♯‘𝑆))
23	21, 22	opeq12d 4819	. . . 4 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩ = ⟨𝑇, (♯‘𝑆)⟩)
24	3, 23	oveq12d 7381	. . 3 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩) = (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩))
25	16, 24	oveq12d 7381	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) ∧ (𝑠 = 𝑆 ∧ 𝑏 = ⟨𝐹, 𝑇, 𝑅⟩)) → (((𝑠 prefix (1st ‘(1st ‘𝑏))) ++ (2nd ‘𝑏)) ++ (𝑠 substr ⟨(2nd ‘(1st ‘𝑏)), (♯‘𝑠)⟩)) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))
26		elex 3453	. . 3 ⊢ (𝑆 ∈ 𝑉 → 𝑆 ∈ V)
27	26	adantr 481	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → 𝑆 ∈ V)
28		otex 5412	. . 3 ⊢ ⟨𝐹, 𝑇, 𝑅⟩ ∈ V
29	28	a1i 11	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → ⟨𝐹, 𝑇, 𝑅⟩ ∈ V)
30		ovexd 7398	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)) ∈ V)
31	2, 25, 27, 29, 30	ovmpod 7515	1 ⊢ ((𝑆 ∈ 𝑉 ∧ (𝐹 ∈ 𝑊 ∧ 𝑇 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌)) → (𝑆 splice ⟨𝐹, 𝑇, 𝑅⟩) = (((𝑆 prefix 𝐹) ++ 𝑅) ++ (𝑆 substr ⟨𝑇, (♯‘𝑆)⟩)))

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  Vcvv 3432  ⟨cop 4568  ⟨cotp 4570  ‘cfv 6492  (class class class)co 7363   ∈ cmpo 7365  1^st c1st 7936  2^nd c2nd 7937  ♯chash 14290   ++ cconcat 14530   substr csubstr 14601   prefix cpfx 14631   splice csplice 14709

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-10 2152  ax-11 2168  ax-12 2189  ax-ext 2712  ax-sep 5225  ax-nul 5235  ax-pr 5369  ax-un 7685

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-nf 1791  df-sb 2074  df-mo 2543  df-eu 2573  df-clab 2719  df-cleq 2732  df-clel 2815  df-nfc 2889  df-ne 2936  df-ral 3055  df-rex 3065  df-rab 3393  df-v 3434  df-sbc 3731  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-ot 4571  df-uni 4846  df-br 5080  df-opab 5142  df-mpt 5161  df-id 5520  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-iota 6448  df-fun 6494  df-fv 6500  df-ov 7366  df-oprab 7367  df-mpo 7368  df-1st 7938  df-2nd 7939  df-splice 14710

This theorem is referenced by:  splid  14713  spllen  14714  splfv1  14715  splfv2a  14716  splval2  14717  gsumspl  18810  efgredleme  19716  efgredlemc  19718  efgcpbllemb  19728  frgpuplem  19745  splfv3  33044  cycpmco2f1  33212  cycpmco2rn  33213  cycpmco2lem2  33215  cycpmco2lem3  33216  cycpmco2lem4  33217  cycpmco2lem5  33218  cycpmco2lem6  33219  cycpmco2  33221