Theorem mapdhval0

Description: Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015)

	Ref	Expression
Hypotheses	mapdh.q	⊢ 𝑄 = ( 0g ‘ 𝐶 )
	mapdh.i	⊢ 𝐼 = ( 𝑥 ∈ V ↦ if ( ( 2nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st ‘ 𝑥 ) ) − ( 2nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) )
	mapdh0.o	⊢ 0 = ( 0g ‘ 𝑈 )
	mapdh0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	mapdh0.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
Assertion	mapdhval0	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 0 ⟩ ) = 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		mapdh.q	⊢ 𝑄 = ( 0g ‘ 𝐶 )
2		mapdh.i	⊢ 𝐼 = ( 𝑥 ∈ V ↦ if ( ( 2nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st ‘ 𝑥 ) ) − ( 2nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) )
3		mapdh0.o	⊢ 0 = ( 0g ‘ 𝑈 )
4		mapdh0.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
5		mapdh0.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
6	3	fvexi	⊢ 0 ∈ V
7	6	a1i	⊢ ( 𝜑 → 0 ∈ V )
8	1 2 4 5 7	mapdhval	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 0 ⟩ ) = if ( 0 = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 0 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 0 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) ) )
9		eqid	⊢ 0 = 0
10	9	iftruei	⊢ if ( 0 = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 0 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 0 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) ) = 𝑄
11	8 10	eqtrdi	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 0 ⟩ ) = 𝑄 )