Metamath Proof Explorer

Theorem cntzsubg

Description: Centralizers in a group are subgroups. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Hypotheses cntzrec.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
cntzrec.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
Assertion cntzsubg ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) ∈ ( SubGrp ‘ 𝑀 ) )

Proof

Step Hyp Ref Expression
1 cntzrec.b ⊢ 𝐵 = ( Base ‘ 𝑀 )
2 cntzrec.z ⊢ 𝑍 = ( Cntz ‘ 𝑀 )
3 grpmnd ⊢ ( 𝑀 ∈ Grp → 𝑀 ∈ Mnd )
4 1 2 cntzsubm ⊢ ( ( 𝑀 ∈ Mnd ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝑀 ) )
5 3 4 sylan ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝑀 ) )
6 simpll ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → 𝑀 ∈ Grp )
7 1 2 cntzssv ⊢ ( 𝑍 ‘ 𝑆 ) ⊆ 𝐵
8 simprl ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) )
9 7 8 sseldi ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → 𝑥 ∈ 𝐵 )
10 eqid ⊢ ( invg ‘ 𝑀 ) = ( invg ‘ 𝑀 )
11 1 10 grpinvcl ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ 𝐵 )
12 6 9 11 syl2anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ 𝐵 )
13 ssel2 ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝐵 )
14 13 ad2ant2l ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → 𝑦 ∈ 𝐵 )
15 eqid ⊢ ( +g ‘ 𝑀 ) = ( +g ‘ 𝑀 )
16 1 15 grpcl ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑥 ∈ 𝐵 ∧ ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ∈ 𝐵 )
17 6 9 12 16 syl3anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ∈ 𝐵 )
18 1 15 grpass ⊢ ( ( 𝑀 ∈ Grp ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ∈ 𝐵 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) ) )
19 6 12 14 17 18 syl13anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) ) )
20 1 15 grpass ⊢ ( ( 𝑀 ∈ Grp ∧ ( 𝑦 ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ 𝐵 ) ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) = ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) )
21 6 14 9 12 20 syl13anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) = ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) )
22 21 oveq2d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) ) )
23 19 22 eqtr4d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) )
24 15 2 cntzi ⊢ ( ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) )
25 24 adantl ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) )
26 25 oveq1d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) = ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) )
27 26 oveq2d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( ( 𝑦 ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) )
28 23 27 eqtr4d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) )
29 1 15 grpcl ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑦 ∈ 𝐵 ∧ ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ 𝐵 ) → ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ∈ 𝐵 )
30 6 14 12 29 syl3anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ∈ 𝐵 )
31 1 15 grpass ⊢ ( ( 𝑀 ∈ Grp ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑥 ∈ 𝐵 ∧ ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ∈ 𝐵 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) ) )
32 6 12 9 30 31 syl13anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) ) )
33 1 15 grpass ⊢ ( ( 𝑀 ∈ Grp ∧ ( 𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ 𝐵 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) )
34 6 9 14 12 33 syl13anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) = ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) )
35 34 oveq2d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) ) )
36 32 35 eqtr4d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) ( ( 𝑥 ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) )
37 28 36 eqtr4d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) )
38 eqid ⊢ ( 0g ‘ 𝑀 ) = ( 0g ‘ 𝑀 )
39 1 15 38 10 grprinv ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) = ( 0g ‘ 𝑀 ) )
40 6 9 39 syl2anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) = ( 0g ‘ 𝑀 ) )
41 40 oveq2d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) )
42 1 15 grpcl ⊢ ( ( 𝑀 ∈ Grp ∧ ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ) → ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 )
43 6 12 14 42 syl3anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 )
44 1 15 38 grprid ⊢ ( ( 𝑀 ∈ Grp ∧ ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ∈ 𝐵 ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) )
45 6 43 44 syl2anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( 0g ‘ 𝑀 ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) )
46 41 45 eqtrd ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) ( +g ‘ 𝑀 ) ( 𝑥 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) )
47 1 15 38 10 grplinv ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑥 ∈ 𝐵 ) → ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 0g ‘ 𝑀 ) )
48 6 9 47 syl2anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑥 ) = ( 0g ‘ 𝑀 ) )
49 48 oveq1d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) )
50 1 15 38 grplid ⊢ ( ( 𝑀 ∈ Grp ∧ ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ∈ 𝐵 ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) )
51 6 30 50 syl2anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( 0g ‘ 𝑀 ) ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) )
52 49 51 eqtrd ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑥 ) ( +g ‘ 𝑀 ) ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) = ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) )
53 37 46 52 3eqtr3d ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ ( 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ∧ 𝑦 ∈ 𝑆 ) ) → ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) )
54 53 anassrs ⊢ ( ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) )
55 54 ralrimiva ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ) → ∀ 𝑦 ∈ 𝑆 ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) )
56 simplr ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ) → 𝑆 ⊆ 𝐵 )
57 simpll ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ) → 𝑀 ∈ Grp )
58 simpr ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ) → 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) )
59 7 58 sseldi ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ) → 𝑥 ∈ 𝐵 )
60 57 59 11 syl2anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ) → ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ 𝐵 )
61 1 15 2 cntzel ⊢ ( ( 𝑆 ⊆ 𝐵 ∧ ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ 𝐵 ) → ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ ( 𝑍 ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑆 ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) )
62 56 60 61 syl2anc ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ) → ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ ( 𝑍 ‘ 𝑆 ) ↔ ∀ 𝑦 ∈ 𝑆 ( ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ( +g ‘ 𝑀 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑀 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ) ) )
63 55 62 mpbird ⊢ ( ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) ∧ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ) → ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ ( 𝑍 ‘ 𝑆 ) )
64 63 ralrimiva ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → ∀ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ ( 𝑍 ‘ 𝑆 ) )
65 10 issubg3 ⊢ ( 𝑀 ∈ Grp → ( ( 𝑍 ‘ 𝑆 ) ∈ ( SubGrp ‘ 𝑀 ) ↔ ( ( 𝑍 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ ( 𝑍 ‘ 𝑆 ) ) ) )
66 65 adantr ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → ( ( 𝑍 ‘ 𝑆 ) ∈ ( SubGrp ‘ 𝑀 ) ↔ ( ( 𝑍 ‘ 𝑆 ) ∈ ( SubMnd ‘ 𝑀 ) ∧ ∀ 𝑥 ∈ ( 𝑍 ‘ 𝑆 ) ( ( invg ‘ 𝑀 ) ‘ 𝑥 ) ∈ ( 𝑍 ‘ 𝑆 ) ) ) )
67 5 64 66 mpbir2and ⊢ ( ( 𝑀 ∈ Grp ∧ 𝑆 ⊆ 𝐵 ) → ( 𝑍 ‘ 𝑆 ) ∈ ( SubGrp ‘ 𝑀 ) )