Metamath Proof Explorer


Theorem f1ovscpbl

Description: An injection is compatible with any operations on the base set. (Contributed by Mario Carneiro, 15-Aug-2015)

Ref Expression
Hypothesis f1ocpbl.f ( 𝜑𝐹 : 𝑉1-1-onto𝑋 )
Assertion f1ovscpbl ( ( 𝜑 ∧ ( 𝐴𝐾𝐵𝑉𝐶𝑉 ) ) → ( ( 𝐹𝐵 ) = ( 𝐹𝐶 ) → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( 𝐹 ‘ ( 𝐴 + 𝐶 ) ) ) )

Proof

Step Hyp Ref Expression
1 f1ocpbl.f ( 𝜑𝐹 : 𝑉1-1-onto𝑋 )
2 f1of1 ( 𝐹 : 𝑉1-1-onto𝑋𝐹 : 𝑉1-1𝑋 )
3 1 2 syl ( 𝜑𝐹 : 𝑉1-1𝑋 )
4 3 adantr ( ( 𝜑 ∧ ( 𝐴𝐾𝐵𝑉𝐶𝑉 ) ) → 𝐹 : 𝑉1-1𝑋 )
5 simpr2 ( ( 𝜑 ∧ ( 𝐴𝐾𝐵𝑉𝐶𝑉 ) ) → 𝐵𝑉 )
6 simpr3 ( ( 𝜑 ∧ ( 𝐴𝐾𝐵𝑉𝐶𝑉 ) ) → 𝐶𝑉 )
7 f1fveq ( ( 𝐹 : 𝑉1-1𝑋 ∧ ( 𝐵𝑉𝐶𝑉 ) ) → ( ( 𝐹𝐵 ) = ( 𝐹𝐶 ) ↔ 𝐵 = 𝐶 ) )
8 4 5 6 7 syl12anc ( ( 𝜑 ∧ ( 𝐴𝐾𝐵𝑉𝐶𝑉 ) ) → ( ( 𝐹𝐵 ) = ( 𝐹𝐶 ) ↔ 𝐵 = 𝐶 ) )
9 oveq2 ( 𝐵 = 𝐶 → ( 𝐴 + 𝐵 ) = ( 𝐴 + 𝐶 ) )
10 9 fveq2d ( 𝐵 = 𝐶 → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( 𝐹 ‘ ( 𝐴 + 𝐶 ) ) )
11 8 10 syl6bi ( ( 𝜑 ∧ ( 𝐴𝐾𝐵𝑉𝐶𝑉 ) ) → ( ( 𝐹𝐵 ) = ( 𝐹𝐶 ) → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( 𝐹 ‘ ( 𝐴 + 𝐶 ) ) ) )