Theorem grpsubf

Description: Functionality of group subtraction. (Contributed by Mario Carneiro, 9-Sep-2014)

	Ref	Expression
Hypotheses	grpsubcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
	grpsubcl.m	⊢ − = ( -g ‘ 𝐺 )
Assertion	grpsubf	⊢ ( 𝐺 ∈ Grp → − : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		grpsubcl.b	⊢ 𝐵 = ( Base ‘ 𝐺 )
2		grpsubcl.m	⊢ − = ( -g ‘ 𝐺 )
3		eqid	⊢ ( invg ‘ 𝐺 ) = ( invg ‘ 𝐺 )
4	1 3	grpinvcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑦 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝐵 )
5	4	3adant2	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝐵 )
6		eqid	⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
7	1 6	grpcl	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ∈ 𝐵 )
8	5 7	syld3an3	⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ∈ 𝐵 )
9	8	3expb	⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) ) → ( 𝑥 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ∈ 𝐵 )
10	9	ralrimivva	⊢ ( 𝐺 ∈ Grp → ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ∈ 𝐵 )
11	1 6 3 2	grpsubfval	⊢ − = ( 𝑥 ∈ 𝐵 , 𝑦 ∈ 𝐵 ↦ ( 𝑥 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) )
12	11	fmpo	⊢ ( ∀ 𝑥 ∈ 𝐵 ∀ 𝑦 ∈ 𝐵 ( 𝑥 ( +g ‘ 𝐺 ) ( ( invg ‘ 𝐺 ) ‘ 𝑦 ) ) ∈ 𝐵 ↔ − : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )
13	10 12	sylib	⊢ ( 𝐺 ∈ Grp → − : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )