Theorem mgpval

Description: Value of the multiplication group operation. (Contributed by Mario Carneiro, 21-Dec-2014)

	Ref	Expression
Hypotheses	mgpval.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	mgpval.2	⊢ · = ( .r ‘ 𝑅 )
Assertion	mgpval	⊢ 𝑀 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , · ⟩ )

Proof

Step	Hyp	Ref	Expression
1		mgpval.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2		mgpval.2	⊢ · = ( .r ‘ 𝑅 )
3		id	⊢ ( 𝑟 = 𝑅 → 𝑟 = 𝑅 )
4		fveq2	⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = ( .r ‘ 𝑅 ) )
5	4 2	eqtr4di	⊢ ( 𝑟 = 𝑅 → ( .r ‘ 𝑟 ) = · )
6	5	opeq2d	⊢ ( 𝑟 = 𝑅 → ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑟 ) ⟩ = ⟨ ( +g ‘ ndx ) , · ⟩ )
7	3 6	oveq12d	⊢ ( 𝑟 = 𝑅 → ( 𝑟 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑟 ) ⟩ ) = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , · ⟩ ) )
8		df-mgp	⊢ mulGrp = ( 𝑟 ∈ V ↦ ( 𝑟 sSet ⟨ ( +g ‘ ndx ) , ( .r ‘ 𝑟 ) ⟩ ) )
9		ovex	⊢ ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , · ⟩ ) ∈ V
10	7 8 9	fvmpt	⊢ ( 𝑅 ∈ V → ( mulGrp ‘ 𝑅 ) = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , · ⟩ ) )
11		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( mulGrp ‘ 𝑅 ) = ∅ )
12		reldmsets	⊢ Rel dom sSet
13	12	ovprc1	⊢ ( ¬ 𝑅 ∈ V → ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , · ⟩ ) = ∅ )
14	11 13	eqtr4d	⊢ ( ¬ 𝑅 ∈ V → ( mulGrp ‘ 𝑅 ) = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , · ⟩ ) )
15	10 14	pm2.61i	⊢ ( mulGrp ‘ 𝑅 ) = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , · ⟩ )
16	1 15	eqtri	⊢ 𝑀 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , · ⟩ )