Metamath Proof Explorer

Theorem conjnmzb

Description: Alternative condition for elementhood in the normalizer. (Contributed by Mario Carneiro, 18-Jan-2015)

Ref Expression
Hypotheses conjghm.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
conjghm.p ⊢ + = ( +g ‘ 𝐺 )
conjghm.m ⊢ − = ( -g ‘ 𝐺 )
conjsubg.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) )
conjnmz.1 ⊢ 𝑁 = { 𝑦 ∈ 𝑋 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) }
Assertion conjnmzb ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐴 ∈ 𝑁 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹 ) ) )

Proof

Step Hyp Ref Expression
1 conjghm.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 conjghm.p ⊢ + = ( +g ‘ 𝐺 )
3 conjghm.m ⊢ − = ( -g ‘ 𝐺 )
4 conjsubg.f ⊢ 𝐹 = ( 𝑥 ∈ 𝑆 ↦ ( ( 𝐴 + 𝑥 ) − 𝐴 ) )
5 conjnmz.1 ⊢ 𝑁 = { 𝑦 ∈ 𝑋 ∣ ∀ 𝑧 ∈ 𝑋 ( ( 𝑦 + 𝑧 ) ∈ 𝑆 ↔ ( 𝑧 + 𝑦 ) ∈ 𝑆 ) }
6 5 ssrab3 ⊢ 𝑁 ⊆ 𝑋
7 simpr ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → 𝐴 ∈ 𝑁 )
8 6 7 sselid ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → 𝐴 ∈ 𝑋 )
9 1 2 3 4 5 conjnmz ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → 𝑆 = ran 𝐹 )
10 8 9 jca ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑁 ) → ( 𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹 ) )
11 simprl ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹 ) ) → 𝐴 ∈ 𝑋 )
12 simplrr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹 ) ) ∧ 𝑤 ∈ 𝑋 ) → 𝑆 = ran 𝐹 )
13 12 eleq2d ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐴 + 𝑤 ) ∈ 𝑆 ↔ ( 𝐴 + 𝑤 ) ∈ ran 𝐹 ) )
14 subgrcl ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝐺 ∈ Grp )
15 14 ad3antrrr ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐺 ∈ Grp )
16 simpllr ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ 𝑋 )
17 1 subgss ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → 𝑆 ⊆ 𝑋 )
18 17 ad2antrr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → 𝑆 ⊆ 𝑋 )
19 18 sselda ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑥 ∈ 𝑋 )
20 1 2 3 grpaddsubass ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐴 + 𝑥 ) − 𝐴 ) = ( 𝐴 + ( 𝑥 − 𝐴 ) ) )
21 15 16 19 16 20 syl13anc ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐴 + 𝑥 ) − 𝐴 ) = ( 𝐴 + ( 𝑥 − 𝐴 ) ) )
22 21 eqeq1d ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝐴 + 𝑥 ) − 𝐴 ) = ( 𝐴 + 𝑤 ) ↔ ( 𝐴 + ( 𝑥 − 𝐴 ) ) = ( 𝐴 + 𝑤 ) ) )
23 1 3 grpsubcl ⊢ ( ( 𝐺 ∈ Grp ∧ 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝑥 − 𝐴 ) ∈ 𝑋 )
24 15 19 16 23 syl3anc ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) → ( 𝑥 − 𝐴 ) ∈ 𝑋 )
25 simplr ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) → 𝑤 ∈ 𝑋 )
26 1 2 grplcan ⊢ ( ( 𝐺 ∈ Grp ∧ ( ( 𝑥 − 𝐴 ) ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) ) → ( ( 𝐴 + ( 𝑥 − 𝐴 ) ) = ( 𝐴 + 𝑤 ) ↔ ( 𝑥 − 𝐴 ) = 𝑤 ) )
27 15 24 25 16 26 syl13anc ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐴 + ( 𝑥 − 𝐴 ) ) = ( 𝐴 + 𝑤 ) ↔ ( 𝑥 − 𝐴 ) = 𝑤 ) )
28 1 2 3 grpsubadd ⊢ ( ( 𝐺 ∈ Grp ∧ ( 𝑥 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝑤 ∈ 𝑋 ) ) → ( ( 𝑥 − 𝐴 ) = 𝑤 ↔ ( 𝑤 + 𝐴 ) = 𝑥 ) )
29 15 19 16 25 28 syl13anc ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝑥 − 𝐴 ) = 𝑤 ↔ ( 𝑤 + 𝐴 ) = 𝑥 ) )
30 22 27 29 3bitrd ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( ( 𝐴 + 𝑥 ) − 𝐴 ) = ( 𝐴 + 𝑤 ) ↔ ( 𝑤 + 𝐴 ) = 𝑥 ) )
31 eqcom ⊢ ( ( 𝐴 + 𝑤 ) = ( ( 𝐴 + 𝑥 ) − 𝐴 ) ↔ ( ( 𝐴 + 𝑥 ) − 𝐴 ) = ( 𝐴 + 𝑤 ) )
32 eqcom ⊢ ( 𝑥 = ( 𝑤 + 𝐴 ) ↔ ( 𝑤 + 𝐴 ) = 𝑥 )
33 30 31 32 3bitr4g ⊢ ( ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) ∧ 𝑥 ∈ 𝑆 ) → ( ( 𝐴 + 𝑤 ) = ( ( 𝐴 + 𝑥 ) − 𝐴 ) ↔ 𝑥 = ( 𝑤 + 𝐴 ) ) )
34 33 rexbidva ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ 𝐴 ∈ 𝑋 ) ∧ 𝑤 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ 𝑆 ( 𝐴 + 𝑤 ) = ( ( 𝐴 + 𝑥 ) − 𝐴 ) ↔ ∃ 𝑥 ∈ 𝑆 𝑥 = ( 𝑤 + 𝐴 ) ) )
35 34 adantlrr ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ∃ 𝑥 ∈ 𝑆 ( 𝐴 + 𝑤 ) = ( ( 𝐴 + 𝑥 ) − 𝐴 ) ↔ ∃ 𝑥 ∈ 𝑆 𝑥 = ( 𝑤 + 𝐴 ) ) )
36 ovex ⊢ ( 𝐴 + 𝑤 ) ∈ V
37 eqeq1 ⊢ ( 𝑦 = ( 𝐴 + 𝑤 ) → ( 𝑦 = ( ( 𝐴 + 𝑥 ) − 𝐴 ) ↔ ( 𝐴 + 𝑤 ) = ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) )
38 37 rexbidv ⊢ ( 𝑦 = ( 𝐴 + 𝑤 ) → ( ∃ 𝑥 ∈ 𝑆 𝑦 = ( ( 𝐴 + 𝑥 ) − 𝐴 ) ↔ ∃ 𝑥 ∈ 𝑆 ( 𝐴 + 𝑤 ) = ( ( 𝐴 + 𝑥 ) − 𝐴 ) ) )
39 4 rnmpt ⊢ ran 𝐹 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝑆 𝑦 = ( ( 𝐴 + 𝑥 ) − 𝐴 ) }
40 36 38 39 elab2 ⊢ ( ( 𝐴 + 𝑤 ) ∈ ran 𝐹 ↔ ∃ 𝑥 ∈ 𝑆 ( 𝐴 + 𝑤 ) = ( ( 𝐴 + 𝑥 ) − 𝐴 ) )
41 risset ⊢ ( ( 𝑤 + 𝐴 ) ∈ 𝑆 ↔ ∃ 𝑥 ∈ 𝑆 𝑥 = ( 𝑤 + 𝐴 ) )
42 35 40 41 3bitr4g ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐴 + 𝑤 ) ∈ ran 𝐹 ↔ ( 𝑤 + 𝐴 ) ∈ 𝑆 ) )
43 13 42 bitrd ⊢ ( ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹 ) ) ∧ 𝑤 ∈ 𝑋 ) → ( ( 𝐴 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝐴 ) ∈ 𝑆 ) )
44 43 ralrimiva ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹 ) ) → ∀ 𝑤 ∈ 𝑋 ( ( 𝐴 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝐴 ) ∈ 𝑆 ) )
45 5 elnmz ⊢ ( 𝐴 ∈ 𝑁 ↔ ( 𝐴 ∈ 𝑋 ∧ ∀ 𝑤 ∈ 𝑋 ( ( 𝐴 + 𝑤 ) ∈ 𝑆 ↔ ( 𝑤 + 𝐴 ) ∈ 𝑆 ) ) )
46 11 44 45 sylanbrc ⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹 ) ) → 𝐴 ∈ 𝑁 )
47 10 46 impbida ⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐺 ) → ( 𝐴 ∈ 𝑁 ↔ ( 𝐴 ∈ 𝑋 ∧ 𝑆 = ran 𝐹 ) ) )