Theorem grpsubval

Description: Group subtraction (division) operation. (Contributed by NM, 31-Mar-2014) (Revised by Mario Carneiro, 13-Dec-2014)

	Ref	Expression
Hypotheses	grpsubval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpsubval.p	⊢ + = ( +g ‘ 𝐺 )
	grpsubval.i	⊢ 𝐼 = ( invg ‘ 𝐺 )
	grpsubval.m	⊢ − = ( -g ‘ 𝐺 )
Assertion	grpsubval	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 + ( 𝐼 ‘ 𝑌 ) ) )

Proof

Step	Hyp	Ref	Expression
1		grpsubval.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpsubval.p	⊢ + = ( +g ‘ 𝐺 )
3		grpsubval.i	⊢ 𝐼 = ( invg ‘ 𝐺 )
4		grpsubval.m	⊢ − = ( -g ‘ 𝐺 )
5		oveq1	⊢ ( 𝑥 = 𝑋 → ( 𝑥 + ( 𝐼 ‘ 𝑦 ) ) = ( 𝑋 + ( 𝐼 ‘ 𝑦 ) ) )
6		fveq2	⊢ ( 𝑦 = 𝑌 → ( 𝐼 ‘ 𝑦 ) = ( 𝐼 ‘ 𝑌 ) )
7	6	oveq2d	⊢ ( 𝑦 = 𝑌 → ( 𝑋 + ( 𝐼 ‘ 𝑦 ) ) = ( 𝑋 + ( 𝐼 ‘ 𝑌 ) ) )
8	1 2 3 4	grpsubfval	⊢ − = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 + ( 𝐼 ‘ 𝑦 ) ) )
9		ovex	⊢ ( 𝑋 + ( 𝐼 ‘ 𝑌 ) ) ∈ V
10	5 7 8 9	ovmpo	⊢ ( ( 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 − 𝑌 ) = ( 𝑋 + ( 𝐼 ‘ 𝑌 ) ) )