Theorem mgpplusg

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

	Ref	Expression
Hypotheses	mgpval.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
	mgpval.2	⊢ · = ( .r ‘ 𝑅 )
Assertion	mgpplusg	⊢ · = ( +g ‘ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		mgpval.1	⊢ 𝑀 = ( mulGrp ‘ 𝑅 )
2		mgpval.2	⊢ · = ( .r ‘ 𝑅 )
3	2	fvexi	⊢ · ∈ V
4		plusgid	⊢ +g = Slot ( +g ‘ ndx )
5	4	setsid	⊢ ( ( 𝑅 ∈ V ∧ · ∈ V ) → · = ( +g ‘ ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , · ⟩ ) ) )
6	3 5	mpan2	⊢ ( 𝑅 ∈ V → · = ( +g ‘ ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , · ⟩ ) ) )
7	1 2	mgpval	⊢ 𝑀 = ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , · ⟩ )
8	7	fveq2i	⊢ ( +g ‘ 𝑀 ) = ( +g ‘ ( 𝑅 sSet ⟨ ( +g ‘ ndx ) , · ⟩ ) )
9	6 8	eqtr4di	⊢ ( 𝑅 ∈ V → · = ( +g ‘ 𝑀 ) )
10	4	str0	⊢ ∅ = ( +g ‘ ∅ )
11		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( .r ‘ 𝑅 ) = ∅ )
12	2 11	eqtrid	⊢ ( ¬ 𝑅 ∈ V → · = ∅ )
13		fvprc	⊢ ( ¬ 𝑅 ∈ V → ( mulGrp ‘ 𝑅 ) = ∅ )
14	1 13	eqtrid	⊢ ( ¬ 𝑅 ∈ V → 𝑀 = ∅ )
15	14	fveq2d	⊢ ( ¬ 𝑅 ∈ V → ( +g ‘ 𝑀 ) = ( +g ‘ ∅ ) )
16	10 12 15	3eqtr4a	⊢ ( ¬ 𝑅 ∈ V → · = ( +g ‘ 𝑀 ) )
17	9 16	pm2.61i	⊢ · = ( +g ‘ 𝑀 )