Metamath Proof Explorer

Theorem issubg3

Description: A subgroup is a symmetric submonoid. (Contributed by Mario Carneiro, 7-Mar-2015)

Ref Expression
Hypothesis issubg3.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
Assertion issubg3 ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 issubg3.i ⊢ 𝐼 = ( invg ‘ 𝐺 )
2 eqid ⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
3 2 subg0cl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
4 3 a1i ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 ) )
5 2 subm0cl ⊢ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
6 5 adantr ⊢ ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
7 6 a1i ⊢ ( 𝐺 ∈ Grp → ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) → ( 0g ‘ 𝐺 ) ∈ 𝑆 ) )
8 ne0i ⊢ ( ( 0g ‘ 𝐺 ) ∈ 𝑆 → 𝑆 ≠ ∅ )
9 id ⊢ ( ( 0g ‘ 𝐺 ) ∈ 𝑆 → ( 0g ‘ 𝐺 ) ∈ 𝑆 )
10 8 9 2thd ⊢ ( ( 0g ‘ 𝐺 ) ∈ 𝑆 → ( 𝑆 ≠ ∅ ↔ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) )
11 10 adantl ⊢ ( ( 𝐺 ∈ Grp ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) → ( 𝑆 ≠ ∅ ↔ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) )
12 r19.26 ⊢ ( ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ↔ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )
13 12 a1i ⊢ ( ( 𝐺 ∈ Grp ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ↔ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) )
14 11 13 3anbi23d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) → ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) )
15 anass ⊢ ( ( ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ↔ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) ∧ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) )
16 df-3an ⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ↔ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) )
17 16 anbi1i ⊢ ( ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ↔ ( ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )
18 df-3an ⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ↔ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) ∧ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) )
19 15 17 18 3bitr4ri ⊢ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ↔ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) )
20 14 19 bitrdi ⊢ ( ( 𝐺 ∈ Grp ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) → ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ↔ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) )
21 eqid ⊢ ( Base ‘ 𝐺 ) = ( Base ‘ 𝐺 )
22 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
23 21 22 1 issubg2 ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) )
24 23 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥 ∈ 𝑆 ( ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ∧ ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) )
25 grpmnd ⊢ ( 𝐺 ∈ Grp → 𝐺 ∈ Mnd )
26 21 2 22 issubm ⊢ ( 𝐺 ∈ Mnd → ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ) )
27 25 26 syl ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ) )
28 27 anbi1d ⊢ ( 𝐺 ∈ Grp → ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ↔ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) )
29 28 adantr ⊢ ( ( 𝐺 ∈ Grp ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) → ( ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ↔ ( ( 𝑆 ⊆ ( Base ‘ 𝐺 ) ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ∧ ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑥 ( +g ‘ 𝐺 ) 𝑦 ) ∈ 𝑆 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) )
30 20 24 29 3bitr4d ⊢ ( ( 𝐺 ∈ Grp ∧ ( 0g ‘ 𝐺 ) ∈ 𝑆 ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) )
31 30 ex ⊢ ( 𝐺 ∈ Grp → ( ( 0g ‘ 𝐺 ) ∈ 𝑆 → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) ) )
32 4 7 31 pm5.21ndd ⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ↔ ( 𝑆 ∈ ( SubMnd ‘ 𝐺 ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝐼 ‘ 𝑥 ) ∈ 𝑆 ) ) )