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

Metamath Proof Explorer

Theorem grpodivval

Description: Group division (or subtraction) operation value. (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	grpodivval	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		grpdiv.1	⊢ 𝑋 = ran 𝐺
2		grpdiv.2	⊢ 𝑁 = ( inv ‘ 𝐺 )
3		grpdiv.3	⊢ 𝐷 = ( /_𝑔 ‘ 𝐺 )
4	1 2 3	grpodivfval	⊢ ( 𝐺 ∈ GrpOp → 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) )
5	4	oveqd	⊢ ( 𝐺 ∈ GrpOp → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) 𝐵 ) )
6		oveq1	⊢ ( 𝑥 = 𝐴 → ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝑦 ) ) )
7		fveq2	⊢ ( 𝑦 = 𝐵 → ( 𝑁 ‘ 𝑦 ) = ( 𝑁 ‘ 𝐵 ) )
8	7	oveq2d	⊢ ( 𝑦 = 𝐵 → ( 𝐴 𝐺 ( 𝑁 ‘ 𝑦 ) ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) )
9		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) )
10		ovex	⊢ ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) ∈ V
11	6 8 9 10	ovmpo	⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( 𝑁 ‘ 𝑦 ) ) ) 𝐵 ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) )
12	5 11	sylan9eq	⊢ ( ( 𝐺 ∈ GrpOp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) )
13	12	3impb	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 𝐷 𝐵 ) = ( 𝐴 𝐺 ( 𝑁 ‘ 𝐵 ) ) )