Description: The multiplicative group operator is a function. (Contributed by Mario Carneiro, 11-Mar-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | fnmgp | ⊢ mulGrp Fn V |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | ovex | ⊢ ( 𝑥 sSet 〈 ( +g ‘ ndx ) , ( .r ‘ 𝑥 ) 〉 ) ∈ V | |
2 | df-mgp | ⊢ mulGrp = ( 𝑥 ∈ V ↦ ( 𝑥 sSet 〈 ( +g ‘ ndx ) , ( .r ‘ 𝑥 ) 〉 ) ) | |
3 | 1 2 | fnmpti | ⊢ mulGrp Fn V |