Theorem pcofval 24861

Description: The value of the path concatenation function on a topological space. (Contributed by Jeff Madsen, 15-Jun-2010.) (Revised by Mario Carneiro, 7-Jun-2014.) (Proof shortened by AV, 2-Mar-2024.)

Assertion

Ref	Expression
pcofval	⊢ (*𝑝‘𝐽) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))

Distinct variable group:   𝑓,𝑔,𝑥,𝐽

Proof of Theorem pcofval

Dummy variable 𝑗 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		oveq2 7410	. . . 4 ⊢ (𝑗 = 𝐽 → (II Cn 𝑗) = (II Cn 𝐽))
2		eqidd 2725	. . . 4 ⊢ (𝑗 = 𝐽 → (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))) = (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))
3	1, 1, 2	mpoeq123dv 7477	. . 3 ⊢ (𝑗 = 𝐽 → (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
4		df-pco 24856	. . 3 ⊢ *𝑝 = (𝑗 ∈ Top ↦ (𝑓 ∈ (II Cn 𝑗), 𝑔 ∈ (II Cn 𝑗) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
5		ovex 7435	. . . 4 ⊢ (II Cn 𝐽) ∈ V
6	5, 5	mpoex 8060	. . 3 ⊢ (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) ∈ V
7	3, 4, 6	fvmpt 6989	. 2 ⊢ (𝐽 ∈ Top → (*𝑝‘𝐽) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
8	4	fvmptndm 7019	. . 3 ⊢ (¬ 𝐽 ∈ Top → (*𝑝‘𝐽) = ∅)
9		cntop2 23069	. . . . . . 7 ⊢ (𝑓 ∈ (II Cn 𝐽) → 𝐽 ∈ Top)
10	9	con3i 154	. . . . . 6 ⊢ (¬ 𝐽 ∈ Top → ¬ 𝑓 ∈ (II Cn 𝐽))
11	10	eq0rdv 4397	. . . . 5 ⊢ (¬ 𝐽 ∈ Top → (II Cn 𝐽) = ∅)
12	11	olcd 871	. . . 4 ⊢ (¬ 𝐽 ∈ Top → ((II Cn 𝐽) = ∅ ∨ (II Cn 𝐽) = ∅))
13		0mpo0 7485	. . . 4 ⊢ (((II Cn 𝐽) = ∅ ∨ (II Cn 𝐽) = ∅) → (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) = ∅)
14	12, 13	syl 17	. . 3 ⊢ (¬ 𝐽 ∈ Top → (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))) = ∅)
15	8, 14	eqtr4d 2767	. 2 ⊢ (¬ 𝐽 ∈ Top → (*𝑝‘𝐽) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1))))))
16	7, 15	pm2.61i 182	1 ⊢ (*𝑝‘𝐽) = (𝑓 ∈ (II Cn 𝐽), 𝑔 ∈ (II Cn 𝐽) ↦ (𝑥 ∈ (0[,]1) ↦ if(𝑥 ≤ (1 / 2), (𝑓‘(2 · 𝑥)), (𝑔‘((2 · 𝑥) − 1)))))

Syntax hints:  ¬ wn 3   ∨ wo 844   = wceq 1533   ∈ wcel 2098  ∅c0 4315  ifcif 4521   class class class wbr 5139   ↦ cmpt 5222  ‘cfv 6534  (class class class)co 7402   ∈ cmpo 7404  0cc0 11107  1c1 11108   · cmul 11112   ≤ cle 11247   − cmin 11442   / cdiv 11869  2c2 12265  [,]cicc 13325  Topctop 22719   Cn ccn 23052  IIcii 24719  *_𝑝cpco 24851

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-rep 5276  ax-sep 5290  ax-nul 5297  ax-pow 5354  ax-pr 5418  ax-un 7719

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2526  df-eu 2555  df-clab 2702  df-cleq 2716  df-clel 2802  df-nfc 2877  df-ne 2933  df-ral 3054  df-rex 3063  df-reu 3369  df-rab 3425  df-v 3468  df-sbc 3771  df-csb 3887  df-dif 3944  df-un 3946  df-in 3948  df-ss 3958  df-nul 4316  df-if 4522  df-pw 4597  df-sn 4622  df-pr 4624  df-op 4628  df-uni 4901  df-iun 4990  df-br 5140  df-opab 5202  df-mpt 5223  df-id 5565  df-xp 5673  df-rel 5674  df-cnv 5675  df-co 5676  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680  df-iota 6486  df-fun 6536  df-fn 6537  df-f 6538  df-f1 6539  df-fo 6540  df-f1o 6541  df-fv 6542  df-ov 7405  df-oprab 7406  df-mpo 7407  df-1st 7969  df-2nd 7970  df-map 8819  df-top 22720  df-topon 22737  df-cn 23055  df-pco 24856

This theorem is referenced by:  pcoval  24862