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

Metamath Proof Explorer

Theorem grpodivfval

Description: Group division (or subtraction) operation. (Contributed by NM, 15-Feb-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypotheses grpdiv.1 ⊢ 𝑋 = ran 𝐺
grpdiv.2 ⊢ 𝑁 = ( inv ‘ 𝐺 )
grpdiv.3 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
Assertion grpodivfval ( 𝐺 ∈ GrpOp → 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 grpdiv.1 ⊢ 𝑋 = ran 𝐺
2 grpdiv.2 ⊢ 𝑁 = ( inv ‘ 𝐺 )
3 grpdiv.3 ⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
4 rnexg ⊢ ( 𝐺 ∈ GrpOp → ran 𝐺 ∈ V )
5 1 4 eqeltrid ⊢ ( 𝐺 ∈ GrpOp → 𝑋 ∈ V )
6 mpoexga ⊢ ( ( 𝑋 ∈ V ∧ 𝑋 ∈ V ) → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) ∈ V )
7 5 5 6 syl2anc ⊢ ( 𝐺 ∈ GrpOp → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) ∈ V )
8 rneq ⊢ ( 𝑔 = 𝐺 → ran 𝑔 = ran 𝐺 )
9 8 1 eqtr4di ⊢ ( 𝑔 = 𝐺 → ran 𝑔 = 𝑋 )
10 id ⊢ ( 𝑔 = 𝐺 → 𝑔 = 𝐺 )
11 eqidd ⊢ ( 𝑔 = 𝐺 → 𝑥 = 𝑥 )
12 fveq2 ⊢ ( 𝑔 = 𝐺 → ( inv ‘ 𝑔 ) = ( inv ‘ 𝐺 ) )
13 12 2 eqtr4di ⊢ ( 𝑔 = 𝐺 → ( inv ‘ 𝑔 ) = 𝑁 )
14 13 fveq1d ⊢ ( 𝑔 = 𝐺 → ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) = ( 𝑁 ‘ 𝑦 ) )
15 10 11 14 oveq123d ⊢ ( 𝑔 = 𝐺 → ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) ) = ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) )
16 9 9 15 mpoeq123dv ⊢ ( 𝑔 = 𝐺 → ( 𝑥 ∈ ran 𝑔 , 𝑦 ∈ ran 𝑔 ↦ ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) )
17 df-gdiv ⊢ /𝑔 = ( 𝑔 ∈ GrpOp ↦ ( 𝑥 ∈ ran 𝑔 , 𝑦 ∈ ran 𝑔 ↦ ( 𝑥 𝑔 ( ( inv ‘ 𝑔 ) ‘ 𝑦 ) ) ) )
18 16 17 fvmptg ⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) ∈ V ) → ( /𝑔 ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) )
19 7 18 mpdan ⊢ ( 𝐺 ∈ GrpOp → ( /𝑔 ‘ 𝐺 ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) )
20 3 19 eqtrid ⊢ ( 𝐺 ∈ GrpOp → 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) )