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

Metamath Proof Explorer

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 → − : ( 𝐵 × 𝐵 ) ⟶ 𝐵 )