Metamath Proof Explorer

Theorem ercpbl

Description: Translate the function compatibility relation to a quotient set. (Contributed by Mario Carneiro, 24-Feb-2015) (Revised by Mario Carneiro, 12-Aug-2015) (Revised by AV, 12-Jul-2024)

Ref Expression
Hypotheses ercpbl.r ⊢ ( 𝜑 → ∼ Er 𝑉 )
ercpbl.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
ercpbl.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
ercpbl.c ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝑉 )
ercpbl.e ⊢ ( 𝜑 → ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐴 + 𝐵 ) ∼ ( 𝐶 + 𝐷 ) ) )
Assertion ercpbl ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ) → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( 𝐹 ‘ ( 𝐶 + 𝐷 ) ) ) )

Proof

Step Hyp Ref Expression
1 ercpbl.r ⊢ ( 𝜑 → ∼ Er 𝑉 )
2 ercpbl.v ⊢ ( 𝜑 → 𝑉 ∈ 𝑊 )
3 ercpbl.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑉 ↦ [ 𝑥 ] ∼ )
4 ercpbl.c ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑉 ∧ 𝑏 ∈ 𝑉 ) ) → ( 𝑎 + 𝑏 ) ∈ 𝑉 )
5 ercpbl.e ⊢ ( 𝜑 → ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐴 + 𝐵 ) ∼ ( 𝐶 + 𝐷 ) ) )
6 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) → ( 𝐴 + 𝐵 ) ∼ ( 𝐶 + 𝐷 ) ) )
7 1 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ∼ Er 𝑉 )
8 2 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝑉 ∈ 𝑊 )
9 simp2l ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐴 ∈ 𝑉 )
10 7 8 3 9 ercpbllem ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ↔ 𝐴 ∼ 𝐶 ) )
11 simp2r ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → 𝐵 ∈ 𝑉 )
12 7 8 3 11 ercpbllem ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ↔ 𝐵 ∼ 𝐷 ) )
13 10 12 anbi12d ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ) ↔ ( 𝐴 ∼ 𝐶 ∧ 𝐵 ∼ 𝐷 ) ) )
14 4 caovclg ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑉 )
15 14 3adant3 ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( 𝐴 + 𝐵 ) ∈ 𝑉 )
16 7 8 3 15 ercpbllem ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( 𝐹 ‘ ( 𝐶 + 𝐷 ) ) ↔ ( 𝐴 + 𝐵 ) ∼ ( 𝐶 + 𝐷 ) ) )
17 6 13 16 3imtr4d ⊢ ( ( 𝜑 ∧ ( 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ) ∧ ( 𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉 ) ) → ( ( ( 𝐹 ‘ 𝐴 ) = ( 𝐹 ‘ 𝐶 ) ∧ ( 𝐹 ‘ 𝐵 ) = ( 𝐹 ‘ 𝐷 ) ) → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( 𝐹 ‘ ( 𝐶 + 𝐷 ) ) ) )