Proof of Theorem mgpplusg
| Step | Hyp | Ref
| Expression |
| 1 | | mgpval.2 |
. . . . 5
⊢ · =
(.r‘𝑅) |
| 2 | 1 | fvexi 6920 |
. . . 4
⊢ · ∈
V |
| 3 | | plusgid 17324 |
. . . . 5
⊢
+g = Slot (+g‘ndx) |
| 4 | 3 | setsid 17244 |
. . . 4
⊢ ((𝑅 ∈ V ∧ · ∈
V) → · =
(+g‘(𝑅
sSet 〈(+g‘ndx), ·
〉))) |
| 5 | 2, 4 | mpan2 691 |
. . 3
⊢ (𝑅 ∈ V → · =
(+g‘(𝑅
sSet 〈(+g‘ndx), ·
〉))) |
| 6 | | mgpval.1 |
. . . . 5
⊢ 𝑀 = (mulGrp‘𝑅) |
| 7 | 6, 1 | mgpval 20140 |
. . . 4
⊢ 𝑀 = (𝑅 sSet 〈(+g‘ndx), ·
〉) |
| 8 | 7 | fveq2i 6909 |
. . 3
⊢
(+g‘𝑀) = (+g‘(𝑅 sSet 〈(+g‘ndx), ·
〉)) |
| 9 | 5, 8 | eqtr4di 2795 |
. 2
⊢ (𝑅 ∈ V → · =
(+g‘𝑀)) |
| 10 | 3 | str0 17226 |
. . 3
⊢ ∅ =
(+g‘∅) |
| 11 | | fvprc 6898 |
. . . 4
⊢ (¬
𝑅 ∈ V →
(.r‘𝑅) =
∅) |
| 12 | 1, 11 | eqtrid 2789 |
. . 3
⊢ (¬
𝑅 ∈ V → · =
∅) |
| 13 | | fvprc 6898 |
. . . . 5
⊢ (¬
𝑅 ∈ V →
(mulGrp‘𝑅) =
∅) |
| 14 | 6, 13 | eqtrid 2789 |
. . . 4
⊢ (¬
𝑅 ∈ V → 𝑀 = ∅) |
| 15 | 14 | fveq2d 6910 |
. . 3
⊢ (¬
𝑅 ∈ V →
(+g‘𝑀) =
(+g‘∅)) |
| 16 | 10, 12, 15 | 3eqtr4a 2803 |
. 2
⊢ (¬
𝑅 ∈ V → · =
(+g‘𝑀)) |
| 17 | 9, 16 | pm2.61i 182 |
1
⊢ · =
(+g‘𝑀) |