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