Metamath Proof Explorer


Theorem issubg

Description: The subgroup predicate. (Contributed by Mario Carneiro, 2-Dec-2014)

Ref Expression
Hypothesis issubg.b 𝐵 = ( Base ‘ 𝐺 )
Assertion issubg ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) )

Proof

Step Hyp Ref Expression
1 issubg.b 𝐵 = ( Base ‘ 𝐺 )
2 df-subg SubGrp = ( 𝑤 ∈ Grp ↦ { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤s 𝑠 ) ∈ Grp } )
3 2 mptrcl ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
4 simp1 ( ( 𝐺 ∈ Grp ∧ 𝑆𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) → 𝐺 ∈ Grp )
5 fveq2 ( 𝑤 = 𝐺 → ( Base ‘ 𝑤 ) = ( Base ‘ 𝐺 ) )
6 5 1 eqtr4di ( 𝑤 = 𝐺 → ( Base ‘ 𝑤 ) = 𝐵 )
7 6 pweqd ( 𝑤 = 𝐺 → 𝒫 ( Base ‘ 𝑤 ) = 𝒫 𝐵 )
8 oveq1 ( 𝑤 = 𝐺 → ( 𝑤s 𝑠 ) = ( 𝐺s 𝑠 ) )
9 8 eleq1d ( 𝑤 = 𝐺 → ( ( 𝑤s 𝑠 ) ∈ Grp ↔ ( 𝐺s 𝑠 ) ∈ Grp ) )
10 7 9 rabeqbidv ( 𝑤 = 𝐺 → { 𝑠 ∈ 𝒫 ( Base ‘ 𝑤 ) ∣ ( 𝑤s 𝑠 ) ∈ Grp } = { 𝑠 ∈ 𝒫 𝐵 ∣ ( 𝐺s 𝑠 ) ∈ Grp } )
11 1 fvexi 𝐵 ∈ V
12 11 pwex 𝒫 𝐵 ∈ V
13 12 rabex { 𝑠 ∈ 𝒫 𝐵 ∣ ( 𝐺s 𝑠 ) ∈ Grp } ∈ V
14 10 2 13 fvmpt ( 𝐺 ∈ Grp → ( SubGrp ‘ 𝐺 ) = { 𝑠 ∈ 𝒫 𝐵 ∣ ( 𝐺s 𝑠 ) ∈ Grp } )
15 14 eleq2d ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ( 𝐺s 𝑠 ) ∈ Grp } ) )
16 oveq2 ( 𝑠 = 𝑆 → ( 𝐺s 𝑠 ) = ( 𝐺s 𝑆 ) )
17 16 eleq1d ( 𝑠 = 𝑆 → ( ( 𝐺s 𝑠 ) ∈ Grp ↔ ( 𝐺s 𝑆 ) ∈ Grp ) )
18 17 elrab ( 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ( 𝐺s 𝑠 ) ∈ Grp } ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) )
19 11 elpw2 ( 𝑆 ∈ 𝒫 𝐵𝑆𝐵 )
20 19 anbi1i ( ( 𝑆 ∈ 𝒫 𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) ↔ ( 𝑆𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) )
21 18 20 bitri ( 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ( 𝐺s 𝑠 ) ∈ Grp } ↔ ( 𝑆𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) )
22 15 21 bitrdi ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) ) )
23 ibar ( 𝐺 ∈ Grp → ( ( 𝑆𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑆𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) ) ) )
24 22 23 bitrd ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑆𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) ) ) )
25 3anass ( ( 𝐺 ∈ Grp ∧ 𝑆𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) ↔ ( 𝐺 ∈ Grp ∧ ( 𝑆𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) ) )
26 24 25 bitr4di ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) ) )
27 3 4 26 pm5.21nii ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝐺 ∈ Grp ∧ 𝑆𝐵 ∧ ( 𝐺s 𝑆 ) ∈ Grp ) )