0pledm

Description: Adjust the domain of the left argument to match the right, which works better in our theorems. (Contributed by Mario Carneiro, 28-Jul-2014)

	Ref	Expression
Hypotheses	0pledm.1	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
	0pledm.2	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
Assertion	0pledm	⊢ ( 𝜑 → ( 0_𝑝 ∘_r ≤ 𝐹 ↔ ( 𝐴 × { 0 } ) ∘_r ≤ 𝐹 ) )

Proof

Step	Hyp	Ref	Expression
1		0pledm.1	⊢ ( 𝜑 → 𝐴 ⊆ ℂ )
2		0pledm.2	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
3		sseqin2	⊢ ( 𝐴 ⊆ ℂ ↔ ( ℂ ∩ 𝐴 ) = 𝐴 )
4	1 3	sylib	⊢ ( 𝜑 → ( ℂ ∩ 𝐴 ) = 𝐴 )
5	4	raleqdv	⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ( ℂ ∩ 𝐴 ) 0 ≤ ( 𝐹 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
6		0cn	⊢ 0 ∈ ℂ
7		fnconstg	⊢ ( 0 ∈ ℂ → ( ℂ × { 0 } ) Fn ℂ )
8	6 7	ax-mp	⊢ ( ℂ × { 0 } ) Fn ℂ
9		df-0p	⊢ 0_𝑝 = ( ℂ × { 0 } )
10	9	fneq1i	⊢ ( 0_𝑝 Fn ℂ ↔ ( ℂ × { 0 } ) Fn ℂ )
11	8 10	mpbir	⊢ 0_𝑝 Fn ℂ
12	11	a1i	⊢ ( 𝜑 → 0_𝑝 Fn ℂ )
13		cnex	⊢ ℂ ∈ V
14	13	a1i	⊢ ( 𝜑 → ℂ ∈ V )
15		ssexg	⊢ ( ( 𝐴 ⊆ ℂ ∧ ℂ ∈ V ) → 𝐴 ∈ V )
16	1 13 15	sylancl	⊢ ( 𝜑 → 𝐴 ∈ V )
17		eqid	⊢ ( ℂ ∩ 𝐴 ) = ( ℂ ∩ 𝐴 )
18		0pval	⊢ ( 𝑥 ∈ ℂ → ( 0_𝑝 ‘ 𝑥 ) = 0 )
19	18	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( 0_𝑝 ‘ 𝑥 ) = 0 )
20		eqidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑥 ) )
21	12 2 14 16 17 19 20	ofrfval	⊢ ( 𝜑 → ( 0_𝑝 ∘_r ≤ 𝐹 ↔ ∀ 𝑥 ∈ ( ℂ ∩ 𝐴 ) 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
22		fnconstg	⊢ ( 0 ∈ ℂ → ( 𝐴 × { 0 } ) Fn 𝐴 )
23	6 22	ax-mp	⊢ ( 𝐴 × { 0 } ) Fn 𝐴
24	23	a1i	⊢ ( 𝜑 → ( 𝐴 × { 0 } ) Fn 𝐴 )
25		inidm	⊢ ( 𝐴 ∩ 𝐴 ) = 𝐴
26		c0ex	⊢ 0 ∈ V
27	26	fvconst2	⊢ ( 𝑥 ∈ 𝐴 → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = 0 )
28	27	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐴 × { 0 } ) ‘ 𝑥 ) = 0 )
29	24 2 16 16 25 28 20	ofrfval	⊢ ( 𝜑 → ( ( 𝐴 × { 0 } ) ∘_r ≤ 𝐹 ↔ ∀ 𝑥 ∈ 𝐴 0 ≤ ( 𝐹 ‘ 𝑥 ) ) )
30	5 21 29	3bitr4d	⊢ ( 𝜑 → ( 0_𝑝 ∘_r ≤ 𝐹 ↔ ( 𝐴 × { 0 } ) ∘_r ≤ 𝐹 ) )

Metamath Proof Explorer

Theorem 0pledm

Proof