Metamath Proof Explorer

Theorem i1fposd

Description: Deduction form of i1fposd . (Contributed by Mario Carneiro, 6-Aug-2014)

Ref Expression
Hypothesis i1fposd.1 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ 𝐴 ) ∈ dom ∫1 )
Assertion i1fposd ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) ∈ dom ∫1 )

Proof

Step Hyp Ref Expression
1 i1fposd.1 ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ 𝐴 ) ∈ dom ∫1 )
2 nfcv ⊢ Ⅎ 𝑥 0
3 nfcv ⊢ Ⅎ 𝑥 ≤
4 nffvmpt1 ⊢ Ⅎ 𝑥 ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 )
5 2 3 4 nfbr ⊢ Ⅎ 𝑥 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 )
6 5 4 2 nfif ⊢ Ⅎ 𝑥 if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , 0 )
7 nfcv ⊢ Ⅎ 𝑦 if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) , 0 )
8 fveq2 ⊢ ( 𝑦 = 𝑥 → ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) = ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) )
9 8 breq2d ⊢ ( 𝑦 = 𝑥 → ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) ↔ 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) ) )
10 9 8 ifbieq1d ⊢ ( 𝑦 = 𝑥 → if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , 0 ) = if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) , 0 ) )
11 6 7 10 cbvmpt ⊢ ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) , 0 ) )
12 simpr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝑥 ∈ ℝ )
13 i1ff ⊢ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ∈ dom ∫1 → ( 𝑥 ∈ ℝ ↦ 𝐴 ) : ℝ ⟶ ℝ )
14 1 13 syl ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ 𝐴 ) : ℝ ⟶ ℝ )
15 14 fvmptelrn ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → 𝐴 ∈ ℝ )
16 eqid ⊢ ( 𝑥 ∈ ℝ ↦ 𝐴 ) = ( 𝑥 ∈ ℝ ↦ 𝐴 )
17 16 fvmpt2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝐴 ∈ ℝ ) → ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
18 12 15 17 syl2anc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) = 𝐴 )
19 18 breq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) ↔ 0 ≤ 𝐴 ) )
20 19 18 ifbieq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) , 0 ) = if ( 0 ≤ 𝐴 , 𝐴 , 0 ) )
21 20 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑥 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) )
22 11 21 eqtrid ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) )
23 eqid ⊢ ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , 0 ) ) = ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , 0 ) )
24 23 i1fpos ⊢ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ∈ dom ∫1 → ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , 0 ) ) ∈ dom ∫1 )
25 1 24 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ℝ ↦ if ( 0 ≤ ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , ( ( 𝑥 ∈ ℝ ↦ 𝐴 ) ‘ 𝑦 ) , 0 ) ) ∈ dom ∫1 )
26 22 25 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 0 ≤ 𝐴 , 𝐴 , 0 ) ) ∈ dom ∫1 )