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 𝐹 ) ) )