psmetres2 - Intuitionistic Logic Explorer

	Intuitionistic Logic Explorer		< Previous Next > Nearby theorems
Mirrors > Home > ILE Home > Th. List > psmetres2		GIF version

Theorem psmetres2 14890

Description: Restriction of a pseudometric. (Contributed by Thierry Arnoux, 11-Feb-2018.)

**Assertion**
Ref	Expression
psmetres2	⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅))

Proof of Theorem psmetres2 Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		psmetf 14882	. . . 4 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
2	1	adantr 276	. . 3 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ^*)
3		simpr 110	. . . 4 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → 𝑅 ⊆ 𝑋)
4		xpss12 4795	. . . 4 ⊢ ((𝑅 ⊆ 𝑋 ∧ 𝑅 ⊆ 𝑋) → (𝑅 × 𝑅) ⊆ (𝑋 × 𝑋))
5	3, 3, 4	syl2anc 411	. . 3 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝑅 × 𝑅) ⊆ (𝑋 × 𝑋))
6	2, 5	fssresd 5469	. 2 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)):(𝑅 × 𝑅)⟶ℝ^*)
7		simpr 110	. . . . . 6 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → 𝑎 ∈ 𝑅)
8	7, 7	ovresd 6105	. . . . 5 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑎) = (𝑎𝐷𝑎))
9		simpll 527	. . . . . 6 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → 𝐷 ∈ (PsMet‘𝑋))
10	3	sselda 3197	. . . . . 6 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → 𝑎 ∈ 𝑋)
11		psmet0 14884	. . . . . 6 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) → (𝑎𝐷𝑎) = 0)
12	9, 10, 11	syl2anc 411	. . . . 5 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → (𝑎𝐷𝑎) = 0)
13	8, 12	eqtrd 2239	. . . 4 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑎) = 0)
14	9	ad2antrr 488	. . . . . . . 8 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝐷 ∈ (PsMet‘𝑋))
15	3	ad2antrr 488	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) → 𝑅 ⊆ 𝑋)
16	15	sselda 3197	. . . . . . . 8 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝑐 ∈ 𝑋)
17	10	ad2antrr 488	. . . . . . . 8 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝑎 ∈ 𝑋)
18	3	adantr 276	. . . . . . . . . 10 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → 𝑅 ⊆ 𝑋)
19	18	sselda 3197	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) → 𝑏 ∈ 𝑋)
20	19	adantr 276	. . . . . . . 8 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝑏 ∈ 𝑋)
21		psmettri2 14885	. . . . . . . 8 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +_𝑒 (𝑐𝐷𝑏)))
22	14, 16, 17, 20, 21	syl13anc 1252	. . . . . . 7 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +_𝑒 (𝑐𝐷𝑏)))
23	7	adantr 276	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) → 𝑎 ∈ 𝑅)
24		simpr 110	. . . . . . . . 9 ⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) → 𝑏 ∈ 𝑅)
25	23, 24	ovresd 6105	. . . . . . . 8 ⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) → (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) = (𝑎𝐷𝑏))
26	25	adantr 276	. . . . . . 7 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) = (𝑎𝐷𝑏))
27		simpr 110	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝑐 ∈ 𝑅)
28	7	ad2antrr 488	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝑎 ∈ 𝑅)
29	27, 28	ovresd 6105	. . . . . . . 8 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) = (𝑐𝐷𝑎))
30	24	adantr 276	. . . . . . . . 9 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝑏 ∈ 𝑅)
31	27, 30	ovresd 6105	. . . . . . . 8 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏) = (𝑐𝐷𝑏))
32	29, 31	oveq12d 5980	. . . . . . 7 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +_𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏)) = ((𝑐𝐷𝑎) +_𝑒 (𝑐𝐷𝑏)))
33	22, 26, 32	3brtr4d 4086	. . . . . 6 ⊢ (((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +_𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏)))
34	33	ralrimiva 2580	. . . . 5 ⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) → ∀𝑐 ∈ 𝑅 (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +_𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏)))
35	34	ralrimiva 2580	. . . 4 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → ∀𝑏 ∈ 𝑅 ∀𝑐 ∈ 𝑅 (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +_𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏)))
36	13, 35	jca 306	. . 3 ⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → ((𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑎) = 0 ∧ ∀𝑏 ∈ 𝑅 ∀𝑐 ∈ 𝑅 (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +_𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏))))
37	36	ralrimiva 2580	. 2 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → ∀𝑎 ∈ 𝑅 ((𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑎) = 0 ∧ ∀𝑏 ∈ 𝑅 ∀𝑐 ∈ 𝑅 (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +_𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏))))
38		df-psmet 14390	. . . . . 6 ⊢ PsMet = (𝑎 ∈ V ↦ {𝑏 ∈ (ℝ^* ↑_𝑚 (𝑎 × 𝑎)) ∣ ∀𝑐 ∈ 𝑎 ((𝑐𝑏𝑐) = 0 ∧ ∀𝑑 ∈ 𝑎 ∀𝑒 ∈ 𝑎 (𝑐𝑏𝑑) ≤ ((𝑒𝑏𝑐) +_𝑒 (𝑒𝑏𝑑)))})
39	38	mptrcl 5680	. . . . 5 ⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ V)
40	39	adantr 276	. . . 4 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → 𝑋 ∈ V)
41	40, 3	ssexd 4195	. . 3 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → 𝑅 ∈ V)
42		ispsmet 14880	. . 3 ⊢ (𝑅 ∈ V → ((𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅) ↔ ((𝐷 ↾ (𝑅 × 𝑅)):(𝑅 × 𝑅)⟶ℝ^* ∧ ∀𝑎 ∈ 𝑅 ((𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑎) = 0 ∧ ∀𝑏 ∈ 𝑅 ∀𝑐 ∈ 𝑅 (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +_𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏))))))
43	41, 42	syl 14	. 2 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → ((𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅) ↔ ((𝐷 ↾ (𝑅 × 𝑅)):(𝑅 × 𝑅)⟶ℝ^* ∧ ∀𝑎 ∈ 𝑅 ((𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑎) = 0 ∧ ∀𝑏 ∈ 𝑅 ∀𝑐 ∈ 𝑅 (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +_𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏))))))
44	6, 37, 43	mpbir2and 947	1 ⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅))

Colors of variables: wff set class

Syntax hints: → wi 4 ∧ wa 104 ↔ wb 105 = wceq 1373 ∈ wcel 2177 ∀wral 2485 {crab 2489 Vcvv 2773 ⊆ wss 3170 class class class wbr 4054 × cxp 4686 ↾ cres 4690 ⟶wf 5281 ‘cfv 5285 (class class class)co 5962 ↑_𝑚 cmap 6753 0cc0 7955 ℝ^*cxr 8136 ≤ cle 8138 +_𝑒 cxad 9922 PsMetcpsmet 14382

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-ia1 106 ax-ia2 107 ax-ia3 108 ax-in1 615 ax-in2 616 ax-io 711 ax-5 1471 ax-7 1472 ax-gen 1473 ax-ie1 1517 ax-ie2 1518 ax-8 1528 ax-10 1529 ax-11 1530 ax-i12 1531 ax-bndl 1533 ax-4 1534 ax-17 1550 ax-i9 1554 ax-ial 1558 ax-i5r 1559 ax-13 2179 ax-14 2180 ax-ext 2188 ax-sep 4173 ax-pow 4229 ax-pr 4264 ax-un 4493 ax-setind 4598 ax-cnex 8046 ax-resscn 8047

This theorem depends on definitions: df-bi 117 df-3an 983 df-tru 1376 df-fal 1379 df-nf 1485 df-sb 1787 df-eu 2058 df-mo 2059 df-clab 2193 df-cleq 2199 df-clel 2202 df-nfc 2338 df-ne 2378 df-ral 2490 df-rex 2491 df-rab 2494 df-v 2775 df-sbc 3003 df-csb 3098 df-dif 3172 df-un 3174 df-in 3176 df-ss 3183 df-pw 3623 df-sn 3644 df-pr 3645 df-op 3647 df-uni 3860 df-br 4055 df-opab 4117 df-mpt 4118 df-id 4353 df-xp 4694 df-rel 4695 df-cnv 4696 df-co 4697 df-dm 4698 df-rn 4699 df-res 4700 df-ima 4701 df-iota 5246 df-fun 5287 df-fn 5288 df-f 5289 df-fv 5293 df-ov 5965 df-oprab 5966 df-mpo 5967 df-map 6755 df-pnf 8139 df-mnf 8140 df-xr 8141 df-psmet 14390

This theorem is referenced by: (None)

W3C validator