mapdhval

Description: Lemmma for ~? mapdh . (Contributed by NM, 3-Apr-2015) (Revised by Mario Carneiro, 6-May-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 ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) )
	mapdh.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
	mapdh.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
	mapdh.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐸 )
Assertion	mapdhval	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = if ( 𝑌 = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) ) )

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		mapdh.x	⊢ ( 𝜑 → 𝑋 ∈ 𝐴 )
4		mapdh.f	⊢ ( 𝜑 → 𝐹 ∈ 𝐵 )
5		mapdh.y	⊢ ( 𝜑 → 𝑌 ∈ 𝐸 )
6		otex	⊢ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ∈ V
7		fveq2	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( 2^nd ‘ 𝑥 ) = ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) )
8	7	eqeq1d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( ( 2^nd ‘ 𝑥 ) = 0 ↔ ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = 0 ) )
9	7	sneqd	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → { ( 2^nd ‘ 𝑥 ) } = { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } )
10	9	fveq2d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) = ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) )
11	10	fveqeq2d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) ) = ( 𝐽 ‘ { ℎ } ) ) )
12		fveq2	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( 1^st ‘ 𝑥 ) = ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) )
13	12	fveq2d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) = ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) )
14	13 7	oveq12d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) = ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) )
15	14	sneqd	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } = { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } )
16	15	fveq2d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) = ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) )
17	16	fveq2d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) )
18	12	fveq2d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) = ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) )
19	18	oveq1d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) = ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) )
20	19	sneqd	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } = { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } )
21	20	fveq2d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) )
22	17 21	eqeq12d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) ) )
23	11 22	anbi12d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ↔ ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) ) ) )
24	23	riotabidv	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) = ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) ) ) )
25	8 24	ifbieq2d	⊢ ( 𝑥 = ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ → if ( ( 2^nd ‘ 𝑥 ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ 𝑥 ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ 𝑥 ) ) − ( 2^nd ‘ 𝑥 ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ 𝑥 ) ) 𝑅 ℎ ) } ) ) ) ) = if ( ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) ) ) ) )
26	1	fvexi	⊢ 𝑄 ∈ V
27		riotaex	⊢ ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) ) ) ∈ V
28	26 27	ifex	⊢ if ( ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) ) ) ) ∈ V
29	25 2 28	fvmpt	⊢ ( ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ∈ V → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = if ( ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) ) ) ) )
30	6 29	mp1i	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = if ( ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) ) ) ) )
31		ot3rdg	⊢ ( 𝑌 ∈ 𝐸 → ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = 𝑌 )
32	5 31	syl	⊢ ( 𝜑 → ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = 𝑌 )
33	32	eqeq1d	⊢ ( 𝜑 → ( ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = 0 ↔ 𝑌 = 0 ) )
34	32	sneqd	⊢ ( 𝜑 → { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } = { 𝑌 } )
35	34	fveq2d	⊢ ( 𝜑 → ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) = ( 𝑁 ‘ { 𝑌 } ) )
36	35	fveqeq2d	⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) ) = ( 𝐽 ‘ { ℎ } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ) )
37		ot1stg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐹 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸 ) → ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) = 𝑋 )
38	3 4 5 37	syl3anc	⊢ ( 𝜑 → ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) = 𝑋 )
39	38 32	oveq12d	⊢ ( 𝜑 → ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) = ( 𝑋 − 𝑌 ) )
40	39	sneqd	⊢ ( 𝜑 → { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } = { ( 𝑋 − 𝑌 ) } )
41	40	fveq2d	⊢ ( 𝜑 → ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) = ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) )
42	41	fveq2d	⊢ ( 𝜑 → ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) )
43		ot2ndg	⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝐹 ∈ 𝐵 ∧ 𝑌 ∈ 𝐸 ) → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) = 𝐹 )
44	3 4 5 43	syl3anc	⊢ ( 𝜑 → ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) = 𝐹 )
45	44	oveq1d	⊢ ( 𝜑 → ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) = ( 𝐹 𝑅 ℎ ) )
46	45	sneqd	⊢ ( 𝜑 → { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } = { ( 𝐹 𝑅 ℎ ) } )
47	46	fveq2d	⊢ ( 𝜑 → ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) )
48	42 47	eqeq12d	⊢ ( 𝜑 → ( ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) ↔ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) )
49	36 48	anbi12d	⊢ ( 𝜑 → ( ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) ) ↔ ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) )
50	49	riotabidv	⊢ ( 𝜑 → ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) ) ) = ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) )
51	33 50	ifbieq2d	⊢ ( 𝜑 → if ( ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( ( 1^st ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) − ( 2^nd ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) } ) ) = ( 𝐽 ‘ { ( ( 2^nd ‘ ( 1^st ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) ) 𝑅 ℎ ) } ) ) ) ) = if ( 𝑌 = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) ) )
52	30 51	eqtrd	⊢ ( 𝜑 → ( 𝐼 ‘ ⟨ 𝑋 , 𝐹 , 𝑌 ⟩ ) = if ( 𝑌 = 0 , 𝑄 , ( ℩ ℎ ∈ 𝐷 ( ( 𝑀 ‘ ( 𝑁 ‘ { 𝑌 } ) ) = ( 𝐽 ‘ { ℎ } ) ∧ ( 𝑀 ‘ ( 𝑁 ‘ { ( 𝑋 − 𝑌 ) } ) ) = ( 𝐽 ‘ { ( 𝐹 𝑅 ℎ ) } ) ) ) ) )

Metamath Proof Explorer

Theorem mapdhval

Proof