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 ( ( 𝜑 ∧ ( 𝐴𝑉𝐵𝑉 ) ∧ ( 𝐶𝑉𝐷𝑉 ) ) → ( ( ( 𝐹𝐴 ) = ( 𝐹𝐶 ) ∧ ( 𝐹𝐵 ) = ( 𝐹𝐷 ) ) → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( 𝐹 ‘ ( 𝐶 + 𝐷 ) ) ) )