Theorem updjudhcoinlf

Description: The composition of the mapping of an element of the disjoint union to the value of the corresponding function and the left injection equals the first function. (Contributed by AV, 27-Jun-2022)

	Ref	Expression
Hypotheses	updjud.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )
	updjud.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐶 )
	updjudhf.h	⊢ 𝐻 = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) )
Assertion	updjudhcoinlf	⊢ ( 𝜑 → ( 𝐻 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 )

Proof

Step	Hyp	Ref	Expression
1		updjud.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ 𝐶 )
2		updjud.g	⊢ ( 𝜑 → 𝐺 : 𝐵 ⟶ 𝐶 )
3		updjudhf.h	⊢ 𝐻 = ( 𝑥 ∈ ( 𝐴 ⊔ 𝐵 ) ↦ if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) )
4	1 2 3	updjudhf	⊢ ( 𝜑 → 𝐻 : ( 𝐴 ⊔ 𝐵 ) ⟶ 𝐶 )
5	4	ffnd	⊢ ( 𝜑 → 𝐻 Fn ( 𝐴 ⊔ 𝐵 ) )
6		inlresf	⊢ ( inl ↾ 𝐴 ) : 𝐴 ⟶ ( 𝐴 ⊔ 𝐵 )
7		ffn	⊢ ( ( inl ↾ 𝐴 ) : 𝐴 ⟶ ( 𝐴 ⊔ 𝐵 ) → ( inl ↾ 𝐴 ) Fn 𝐴 )
8	6 7	mp1i	⊢ ( 𝜑 → ( inl ↾ 𝐴 ) Fn 𝐴 )
9		frn	⊢ ( ( inl ↾ 𝐴 ) : 𝐴 ⟶ ( 𝐴 ⊔ 𝐵 ) → ran ( inl ↾ 𝐴 ) ⊆ ( 𝐴 ⊔ 𝐵 ) )
10	6 9	mp1i	⊢ ( 𝜑 → ran ( inl ↾ 𝐴 ) ⊆ ( 𝐴 ⊔ 𝐵 ) )
11		fnco	⊢ ( ( 𝐻 Fn ( 𝐴 ⊔ 𝐵 ) ∧ ( inl ↾ 𝐴 ) Fn 𝐴 ∧ ran ( inl ↾ 𝐴 ) ⊆ ( 𝐴 ⊔ 𝐵 ) ) → ( 𝐻 ∘ ( inl ↾ 𝐴 ) ) Fn 𝐴 )
12	5 8 10 11	syl3anc	⊢ ( 𝜑 → ( 𝐻 ∘ ( inl ↾ 𝐴 ) ) Fn 𝐴 )
13	1	ffnd	⊢ ( 𝜑 → 𝐹 Fn 𝐴 )
14		fvco2	⊢ ( ( ( inl ↾ 𝐴 ) Fn 𝐴 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐻 ∘ ( inl ↾ 𝐴 ) ) ‘ 𝑎 ) = ( 𝐻 ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑎 ) ) )
15	8 14	sylan	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐻 ∘ ( inl ↾ 𝐴 ) ) ‘ 𝑎 ) = ( 𝐻 ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑎 ) ) )
16		fvres	⊢ ( 𝑎 ∈ 𝐴 → ( ( inl ↾ 𝐴 ) ‘ 𝑎 ) = ( inl ‘ 𝑎 ) )
17	16	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( inl ↾ 𝐴 ) ‘ 𝑎 ) = ( inl ‘ 𝑎 ) )
18	17	fveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐻 ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑎 ) ) = ( 𝐻 ‘ ( inl ‘ 𝑎 ) ) )
19		fveqeq2	⊢ ( 𝑥 = ( inl ‘ 𝑎 ) → ( ( 1st ‘ 𝑥 ) = ∅ ↔ ( 1st ‘ ( inl ‘ 𝑎 ) ) = ∅ ) )
20		2fveq3	⊢ ( 𝑥 = ( inl ‘ 𝑎 ) → ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) )
21		2fveq3	⊢ ( 𝑥 = ( inl ‘ 𝑎 ) → ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) )
22	19 20 21	ifbieq12d	⊢ ( 𝑥 = ( inl ‘ 𝑎 ) → if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) = if ( ( 1st ‘ ( inl ‘ 𝑎 ) ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) , ( 𝐺 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) ) )
23	22	adantl	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 = ( inl ‘ 𝑎 ) ) → if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) = if ( ( 1st ‘ ( inl ‘ 𝑎 ) ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) , ( 𝐺 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) ) )
24		1stinl	⊢ ( 𝑎 ∈ 𝐴 → ( 1st ‘ ( inl ‘ 𝑎 ) ) = ∅ )
25	24	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 1st ‘ ( inl ‘ 𝑎 ) ) = ∅ )
26	25	adantr	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 = ( inl ‘ 𝑎 ) ) → ( 1st ‘ ( inl ‘ 𝑎 ) ) = ∅ )
27	26	iftrued	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 = ( inl ‘ 𝑎 ) ) → if ( ( 1st ‘ ( inl ‘ 𝑎 ) ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) , ( 𝐺 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) ) = ( 𝐹 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) )
28	23 27	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) ∧ 𝑥 = ( inl ‘ 𝑎 ) ) → if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) = ( 𝐹 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) )
29		djulcl	⊢ ( 𝑎 ∈ 𝐴 → ( inl ‘ 𝑎 ) ∈ ( 𝐴 ⊔ 𝐵 ) )
30	29	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( inl ‘ 𝑎 ) ∈ ( 𝐴 ⊔ 𝐵 ) )
31	1	adantr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝐹 : 𝐴 ⟶ 𝐶 )
32		2ndinl	⊢ ( 𝑎 ∈ 𝐴 → ( 2nd ‘ ( inl ‘ 𝑎 ) ) = 𝑎 )
33	32	adantl	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 2nd ‘ ( inl ‘ 𝑎 ) ) = 𝑎 )
34		simpr	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → 𝑎 ∈ 𝐴 )
35	33 34	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 2nd ‘ ( inl ‘ 𝑎 ) ) ∈ 𝐴 )
36	31 35	ffvelcdmd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) ∈ 𝐶 )
37	3 28 30 36	fvmptd2	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐻 ‘ ( inl ‘ 𝑎 ) ) = ( 𝐹 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) )
38	18 37	eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐻 ‘ ( ( inl ↾ 𝐴 ) ‘ 𝑎 ) ) = ( 𝐹 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) )
39	33	fveq2d	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( 𝐹 ‘ ( 2nd ‘ ( inl ‘ 𝑎 ) ) ) = ( 𝐹 ‘ 𝑎 ) )
40	15 38 39	3eqtrd	⊢ ( ( 𝜑 ∧ 𝑎 ∈ 𝐴 ) → ( ( 𝐻 ∘ ( inl ↾ 𝐴 ) ) ‘ 𝑎 ) = ( 𝐹 ‘ 𝑎 ) )
41	12 13 40	eqfnfvd	⊢ ( 𝜑 → ( 𝐻 ∘ ( inl ↾ 𝐴 ) ) = 𝐹 )