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

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