Metamath Proof Explorer

Theorem mapdhval2

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

		Ref	Expression
	Hypotheses	mapdh.q	⊢ 𝑄 = ( 0_g ‘ 𝐶 )
		mapdh.i	⊢ 𝐼 = ( 𝑥 ∈ V ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) )
		mapdh2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
		mapdh2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
		mapdh2.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
	Assertion	mapdhval2	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		mapdh.q	⊢ 𝑄 = ( 0_g ‘ 𝐶 )
2		mapdh.i	⊢ 𝐼 = ( 𝑥 ∈ V ↦ if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) )
3		mapdh2.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4		mapdh2.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
5		mapdh2.y	⊢ ( 𝜑 → 𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
6	1 2 3 4 5	mapdhval	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = if ( 𝑌 = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) ) )
7		eldifsni	⊢ ( 𝑌 ∈ ( 𝑉 ∖ { 0 } ) → 𝑌 ≠ 0 )
8	7	neneqd	⊢ ( 𝑌 ∈ ( 𝑉 ∖ { 0 } ) → ¬ 𝑌 = 0 )
9		iffalse	⊢ ( ¬ 𝑌 = 0 → if ( 𝑌 = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) ) = ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) )
10	5 8 9	3syl	⊢ ( 𝜑 → if ( 𝑌 = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) ) = ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) )
11	6 10	eqtrd	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) )