Theorem grpodivf

Description: Mapping for group division. (Contributed by NM, 10-Apr-2008) (Revised by Mario Carneiro, 15-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypotheses	grpdivf.1	⊢ 𝑋 = ran 𝐺
	grpdivf.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
Assertion	grpodivf	⊢ ( 𝐺 ∈ GrpOp → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )

Proof

Step	Hyp	Ref	Expression
1		grpdivf.1	⊢ 𝑋 = ran 𝐺
2		grpdivf.3	⊢ 𝐷 = ( /𝑔 ‘ 𝐺 )
3		eqid	⊢ ( inv ‘ 𝐺 ) = ( inv ‘ 𝐺 )
4	1 3	grpoinvcl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑦 ∈ 𝑋 ) → ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 )
5	4	3adant2	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 )
6	1	grpocl	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ∧ ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ∈ 𝑋 ) → ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ∈ 𝑋 )
7	5 6	syld3an3	⊢ ( ( 𝐺 ∈ GrpOp ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ∈ 𝑋 )
8	7	3expib	⊢ ( 𝐺 ∈ GrpOp → ( ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ∈ 𝑋 ) )
9	8	ralrimivv	⊢ ( 𝐺 ∈ GrpOp → ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ∈ 𝑋 )
10		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) )
11	10	fmpo	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑋 ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ∈ 𝑋 ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
12	9 11	sylib	⊢ ( 𝐺 ∈ GrpOp → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )
13	1 3 2	grpodivfval	⊢ ( 𝐺 ∈ GrpOp → 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ) )
14	13	feq1d	⊢ ( 𝐺 ∈ GrpOp → ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ↔ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 𝐺 ( ( inv ‘ 𝐺 ) ‘ 𝑦 ) ) ) : ( 𝑋 × 𝑋 ) ⟶ 𝑋 ) )
15	12 14	mpbird	⊢ ( 𝐺 ∈ GrpOp → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ 𝑋 )