Metamath Proof Explorer

Theorem mgpf

Description: Restricted functionality of the multiplicative group on rings. (Contributed by Mario Carneiro, 11-Mar-2015)

Ref Expression
Assertion mgpf ⊢ mulGrp ↾ Ring : Ring ⟶ Mnd

Proof

Step Hyp Ref Expression
1 fnmgp ⊢ mulGrp Fn V
2 ssv ⊢ Ring ⊆ V
3 fnssres ⊢ mulGrp Fn V ∧ Ring ⊆ V → mulGrp ↾ Ring Fn Ring
4 1 2 3 mp2an ⊢ mulGrp ↾ Ring Fn Ring
5 fvres ⊢ a ∈ Ring → mulGrp ↾ Ring ⁡ a = mulGrp a
6 eqid ⊢ mulGrp a = mulGrp a
7 6 ringmgp ⊢ a ∈ Ring → mulGrp a ∈ Mnd
8 5 7 eqeltrd ⊢ a ∈ Ring → mulGrp ↾ Ring ⁡ a ∈ Mnd
9 8 rgen ⊢ ∀ a ∈ Ring mulGrp ↾ Ring ⁡ a ∈ Mnd
10 ffnfv ⊢ mulGrp ↾ Ring : Ring ⟶ Mnd ↔ mulGrp ↾ Ring Fn Ring ∧ ∀ a ∈ Ring mulGrp ↾ Ring ⁡ a ∈ Mnd
11 4 9 10 mpbir2an ⊢ mulGrp ↾ Ring : Ring ⟶ Mnd