Theorem pfxval 13858

Description: Value of a prefix operation. (Contributed by AV, 2-May-2020.)

Assertion

Ref	Expression
pfxval	⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 prefix 𝐿) = (𝑆 substr ⟨0, 𝐿⟩))

Proof of Theorem pfxval

Dummy variables 𝑙 𝑠 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		df-pfx 13856	. . 3 ⊢ prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩))
2	1	a1i 11	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → prefix = (𝑠 ∈ V, 𝑙 ∈ ℕ0 ↦ (𝑠 substr ⟨0, 𝑙⟩)))
3		simpl 475	. . . 4 ⊢ ((𝑠 = 𝑆 ∧ 𝑙 = 𝐿) → 𝑠 = 𝑆)
4		opeq2 4679	. . . . 5 ⊢ (𝑙 = 𝐿 → ⟨0, 𝑙⟩ = ⟨0, 𝐿⟩)
5	4	adantl 474	. . . 4 ⊢ ((𝑠 = 𝑆 ∧ 𝑙 = 𝐿) → ⟨0, 𝑙⟩ = ⟨0, 𝐿⟩)
6	3, 5	oveq12d 6996	. . 3 ⊢ ((𝑠 = 𝑆 ∧ 𝑙 = 𝐿) → (𝑠 substr ⟨0, 𝑙⟩) = (𝑆 substr ⟨0, 𝐿⟩))
7	6	adantl 474	. 2 ⊢ (((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) ∧ (𝑠 = 𝑆 ∧ 𝑙 = 𝐿)) → (𝑠 substr ⟨0, 𝑙⟩) = (𝑆 substr ⟨0, 𝐿⟩))
8		elex 3433	. . 3 ⊢ (𝑆 ∈ 𝑉 → 𝑆 ∈ V)
9	8	adantr 473	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → 𝑆 ∈ V)
10		simpr 477	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → 𝐿 ∈ ℕ0)
11		ovexd 7012	. 2 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 substr ⟨0, 𝐿⟩) ∈ V)
12	2, 7, 9, 10, 11	ovmpod 7120	1 ⊢ ((𝑆 ∈ 𝑉 ∧ 𝐿 ∈ ℕ0) → (𝑆 prefix 𝐿) = (𝑆 substr ⟨0, 𝐿⟩))

Syntax hints:   → wi 4   ∧ wa 387   = wceq 1507   ∈ wcel 2050  Vcvv 3415  ⟨cop 4448  (class class class)co 6978   ∈ cmpo 6980  0cc0 10337  ℕ₀cn0 11710   substr csubstr 13806   prefix cpfx 13855

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1965  ax-8 2052  ax-9 2059  ax-10 2079  ax-11 2093  ax-12 2106  ax-13 2301  ax-ext 2750  ax-sep 5061  ax-nul 5068  ax-pr 5187

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2016  df-mo 2547  df-eu 2583  df-clab 2759  df-cleq 2771  df-clel 2846  df-nfc 2918  df-ral 3093  df-rex 3094  df-rab 3097  df-v 3417  df-sbc 3684  df-dif 3834  df-un 3836  df-in 3838  df-ss 3845  df-nul 4181  df-if 4352  df-sn 4443  df-pr 4445  df-op 4449  df-uni 4714  df-br 4931  df-opab 4993  df-id 5313  df-xp 5414  df-rel 5415  df-cnv 5416  df-co 5417  df-dm 5418  df-iota 6154  df-fun 6192  df-fv 6198  df-ov 6981  df-oprab 6982  df-mpo 6983  df-pfx 13856

This theorem is referenced by:  pfx00  13859  pfx0  13860  pfxval0  13861  pfxcl  13862  pfxmpt  13863  pfxfv  13867  pfxnd  13872  pfx1  13888  pfxswrd  13892  swrdpfx  13894  pfxpfx  13896  swrdccat  13941  pfxccatpfx1  13943  pfxccatpfx2  13944  splvalpfxOLD  13965  cshw0  14021  pfxco  14065  clwwlkf1  27574