Description: The free group is a group. (Contributed by Mario Carneiro, 1-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Hypothesis | frgpgrp.g | ⊢ 𝐺 = ( freeGrp ‘ 𝐼 ) | |
Assertion | frgpgrp | ⊢ ( 𝐼 ∈ 𝑉 → 𝐺 ∈ Grp ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | frgpgrp.g | ⊢ 𝐺 = ( freeGrp ‘ 𝐼 ) | |
2 | eqid | ⊢ ( ~FG ‘ 𝐼 ) = ( ~FG ‘ 𝐼 ) | |
3 | 1 2 | frgp0 | ⊢ ( 𝐼 ∈ 𝑉 → ( 𝐺 ∈ Grp ∧ [ ∅ ] ( ~FG ‘ 𝐼 ) = ( 0g ‘ 𝐺 ) ) ) |
4 | 3 | simpld | ⊢ ( 𝐼 ∈ 𝑉 → 𝐺 ∈ Grp ) |