Metamath Proof Explorer


Theorem giclcl

Description: Isomorphism implies the left side is a group. (Contributed by Stefan O'Rear, 25-Jan-2015)

Ref Expression
Assertion giclcl ( 𝑅𝑔 𝑆𝑅 ∈ Grp )

Proof

Step Hyp Ref Expression
1 brgic ( 𝑅𝑔 𝑆 ↔ ( 𝑅 GrpIso 𝑆 ) ≠ ∅ )
2 n0 ( ( 𝑅 GrpIso 𝑆 ) ≠ ∅ ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) )
3 1 2 bitri ( 𝑅𝑔 𝑆 ↔ ∃ 𝑓 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) )
4 gimghm ( 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝑓 ∈ ( 𝑅 GrpHom 𝑆 ) )
5 ghmgrp1 ( 𝑓 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝑅 ∈ Grp )
6 4 5 syl ( 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝑅 ∈ Grp )
7 6 exlimiv ( ∃ 𝑓 𝑓 ∈ ( 𝑅 GrpIso 𝑆 ) → 𝑅 ∈ Grp )
8 3 7 sylbi ( 𝑅𝑔 𝑆𝑅 ∈ Grp )