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

Metamath Proof Explorer

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 ‘ 𝑀 )