This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem updjudhcoinrg

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

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

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 inrresf ⊢ ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 )
7 ffn ⊢ ( ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 ) → ( inr ↾ 𝐵 ) Fn 𝐵 )
8 6 7 mp1i ⊢ ( 𝜑 → ( inr ↾ 𝐵 ) Fn 𝐵 )
9 frn ⊢ ( ( inr ↾ 𝐵 ) : 𝐵 ⟶ ( 𝐴 ⊔ 𝐵 ) → ran ( inr ↾ 𝐵 ) ⊆ ( 𝐴 ⊔ 𝐵 ) )
10 6 9 mp1i ⊢ ( 𝜑 → ran ( inr ↾ 𝐵 ) ⊆ ( 𝐴 ⊔ 𝐵 ) )
11 fnco ⊢ ( ( 𝐻 Fn ( 𝐴 ⊔ 𝐵 ) ∧ ( inr ↾ 𝐵 ) Fn 𝐵 ∧ ran ( inr ↾ 𝐵 ) ⊆ ( 𝐴 ⊔ 𝐵 ) ) → ( 𝐻 ∘ ( inr ↾ 𝐵 ) ) Fn 𝐵 )
12 5 8 10 11 syl3anc ⊢ ( 𝜑 → ( 𝐻 ∘ ( inr ↾ 𝐵 ) ) Fn 𝐵 )
13 2 ffnd ⊢ ( 𝜑 → 𝐺 Fn 𝐵 )
14 fvco2 ⊢ ( ( ( inr ↾ 𝐵 ) Fn 𝐵 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐻 ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑏 ) = ( 𝐻 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑏 ) ) )
15 8 14 sylan ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐻 ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑏 ) = ( 𝐻 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑏 ) ) )
16 fvres ⊢ ( 𝑏 ∈ 𝐵 → ( ( inr ↾ 𝐵 ) ‘ 𝑏 ) = ( inr ‘ 𝑏 ) )
17 16 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( inr ↾ 𝐵 ) ‘ 𝑏 ) = ( inr ‘ 𝑏 ) )
18 17 fveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐻 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑏 ) ) = ( 𝐻 ‘ ( inr ‘ 𝑏 ) ) )
19 fveqeq2 ⊢ ( 𝑥 = ( inr ‘ 𝑏 ) → ( ( 1st ‘ 𝑥 ) = ∅ ↔ ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ ) )
20 2fveq3 ⊢ ( 𝑥 = ( inr ‘ 𝑏 ) → ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) = ( 𝐹 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) )
21 2fveq3 ⊢ ( 𝑥 = ( inr ‘ 𝑏 ) → ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) = ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) )
22 19 20 21 ifbieq12d ⊢ ( 𝑥 = ( inr ‘ 𝑏 ) → if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) = if ( ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) , ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) ) )
23 22 adantl ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑥 = ( inr ‘ 𝑏 ) ) → if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) = if ( ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) , ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) ) )
24 1stinr ⊢ ( 𝑏 ∈ 𝐵 → ( 1st ‘ ( inr ‘ 𝑏 ) ) = 1o )
25 1n0 ⊢ 1o ≠ ∅
26 25 neii ⊢ ¬ 1o = ∅
27 eqeq1 ⊢ ( ( 1st ‘ ( inr ‘ 𝑏 ) ) = 1o → ( ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ ↔ 1o = ∅ ) )
28 26 27 mtbiri ⊢ ( ( 1st ‘ ( inr ‘ 𝑏 ) ) = 1o → ¬ ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ )
29 24 28 syl ⊢ ( 𝑏 ∈ 𝐵 → ¬ ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ )
30 29 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ¬ ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ )
31 30 adantr ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑥 = ( inr ‘ 𝑏 ) ) → ¬ ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ )
32 31 iffalsed ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑥 = ( inr ‘ 𝑏 ) ) → if ( ( 1st ‘ ( inr ‘ 𝑏 ) ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) , ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) ) = ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) )
33 23 32 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) ∧ 𝑥 = ( inr ‘ 𝑏 ) ) → if ( ( 1st ‘ 𝑥 ) = ∅ , ( 𝐹 ‘ ( 2nd ‘ 𝑥 ) ) , ( 𝐺 ‘ ( 2nd ‘ 𝑥 ) ) ) = ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) )
34 djurcl ⊢ ( 𝑏 ∈ 𝐵 → ( inr ‘ 𝑏 ) ∈ ( 𝐴 ⊔ 𝐵 ) )
35 34 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( inr ‘ 𝑏 ) ∈ ( 𝐴 ⊔ 𝐵 ) )
36 2 adantr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝐺 : 𝐵 ⟶ 𝐶 )
37 2ndinr ⊢ ( 𝑏 ∈ 𝐵 → ( 2nd ‘ ( inr ‘ 𝑏 ) ) = 𝑏 )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 2nd ‘ ( inr ‘ 𝑏 ) ) = 𝑏 )
39 simpr ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → 𝑏 ∈ 𝐵 )
40 38 39 eqeltrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 2nd ‘ ( inr ‘ 𝑏 ) ) ∈ 𝐵 )
41 36 40 ffvelcdmd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) ∈ 𝐶 )
42 3 33 35 41 fvmptd2 ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐻 ‘ ( inr ‘ 𝑏 ) ) = ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) )
43 18 42 eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐻 ‘ ( ( inr ↾ 𝐵 ) ‘ 𝑏 ) ) = ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) )
44 38 fveq2d ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( 𝐺 ‘ ( 2nd ‘ ( inr ‘ 𝑏 ) ) ) = ( 𝐺 ‘ 𝑏 ) )
45 15 43 44 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑏 ∈ 𝐵 ) → ( ( 𝐻 ∘ ( inr ↾ 𝐵 ) ) ‘ 𝑏 ) = ( 𝐺 ‘ 𝑏 ) )
46 12 13 45 eqfnfvd ⊢ ( 𝜑 → ( 𝐻 ∘ ( inr ↾ 𝐵 ) ) = 𝐺 )