Metamath Proof Explorer


Theorem mapdhval2

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𝑥 ) ) 𝑅 ) } ) ) ) ) )
mapdh2.x ( 𝜑𝑋𝐴 )
mapdh2.f ( 𝜑𝐹𝐵 )
mapdh2.y ( 𝜑𝑌 ∈ ( 𝑉 ∖ { 0 } ) )
Assertion mapdhval2 ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ) } ) ) ) )

Proof

Step Hyp Ref Expression
1 mapdh.q 𝑄 = ( 0g𝐶 )
2 mapdh.i 𝐼 = ( 𝑥 ∈ V ↦ if ( ( 2nd𝑥 ) = 0 , 𝑄 , ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2nd𝑥 ) } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1st ‘ ( 1st𝑥 ) ) ( 2nd𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2nd ‘ ( 1st𝑥 ) ) 𝑅 ) } ) ) ) ) )
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 ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = ( 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ) } ) ) ) )