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

Metamath Proof Explorer

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 ) , · ⟩ )