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 |
⊢ ( 𝜑 → ( 𝐼 ‘ 〈 𝑋 , 𝐹 , 𝑌 〉 ) = ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) ) |