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 syl5eq ( 𝜑 → ( 𝑦 ∈ ℝ ↦ 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 )