Metamath Proof Explorer


Theorem symgextf1

Description: The extension of a permutation, fixing the additional element, is a 1-1 function. (Contributed by AV, 6-Jan-2019)

Ref Expression
Hypotheses symgext.s 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
symgext.e 𝐸 = ( 𝑥𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍𝑥 ) ) )
Assertion symgextf1 ( ( 𝐾𝑁𝑍𝑆 ) → 𝐸 : 𝑁1-1𝑁 )

Proof

Step Hyp Ref Expression
1 symgext.s 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
2 symgext.e 𝐸 = ( 𝑥𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍𝑥 ) ) )
3 1 2 symgextf ( ( 𝐾𝑁𝑍𝑆 ) → 𝐸 : 𝑁𝑁 )
4 difsnid ( 𝐾𝑁 → ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) = 𝑁 )
5 4 eqcomd ( 𝐾𝑁𝑁 = ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) )
6 5 eleq2d ( 𝐾𝑁 → ( 𝑦𝑁𝑦 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) )
7 5 eleq2d ( 𝐾𝑁 → ( 𝑧𝑁𝑧 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) )
8 6 7 anbi12d ( 𝐾𝑁 → ( ( 𝑦𝑁𝑧𝑁 ) ↔ ( 𝑦 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∧ 𝑧 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ) )
9 8 adantr ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝑦𝑁𝑧𝑁 ) ↔ ( 𝑦 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∧ 𝑧 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) ) )
10 elun ( 𝑦 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↔ ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∨ 𝑦 ∈ { 𝐾 } ) )
11 elun ( 𝑧 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ↔ ( 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ∨ 𝑧 ∈ { 𝐾 } ) )
12 1 2 symgextfv ( ( 𝐾𝑁𝑍𝑆 ) → ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝐸𝑦 ) = ( 𝑍𝑦 ) ) )
13 12 com12 ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( ( 𝐾𝑁𝑍𝑆 ) → ( 𝐸𝑦 ) = ( 𝑍𝑦 ) ) )
14 13 adantr ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝐾𝑁𝑍𝑆 ) → ( 𝐸𝑦 ) = ( 𝑍𝑦 ) ) )
15 14 imp ( ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝐾𝑁𝑍𝑆 ) ) → ( 𝐸𝑦 ) = ( 𝑍𝑦 ) )
16 1 2 symgextfv ( ( 𝐾𝑁𝑍𝑆 ) → ( 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝐸𝑧 ) = ( 𝑍𝑧 ) ) )
17 16 com12 ( 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( ( 𝐾𝑁𝑍𝑆 ) → ( 𝐸𝑧 ) = ( 𝑍𝑧 ) ) )
18 17 adantl ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝐾𝑁𝑍𝑆 ) → ( 𝐸𝑧 ) = ( 𝑍𝑧 ) ) )
19 18 imp ( ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝐾𝑁𝑍𝑆 ) ) → ( 𝐸𝑧 ) = ( 𝑍𝑧 ) )
20 15 19 eqeq12d ( ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝐾𝑁𝑍𝑆 ) ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) ↔ ( 𝑍𝑦 ) = ( 𝑍𝑧 ) ) )
21 eqid ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
22 21 1 symgbasf1o ( 𝑍𝑆𝑍 : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) )
23 f1of1 ( 𝑍 : ( 𝑁 ∖ { 𝐾 } ) –1-1-onto→ ( 𝑁 ∖ { 𝐾 } ) → 𝑍 : ( 𝑁 ∖ { 𝐾 } ) –1-1→ ( 𝑁 ∖ { 𝐾 } ) )
24 dff13 ( 𝑍 : ( 𝑁 ∖ { 𝐾 } ) –1-1→ ( 𝑁 ∖ { 𝐾 } ) ↔ ( 𝑍 : ( 𝑁 ∖ { 𝐾 } ) ⟶ ( 𝑁 ∖ { 𝐾 } ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑍𝑖 ) = ( 𝑍𝑗 ) → 𝑖 = 𝑗 ) ) )
25 fveqeq2 ( 𝑖 = 𝑦 → ( ( 𝑍𝑖 ) = ( 𝑍𝑗 ) ↔ ( 𝑍𝑦 ) = ( 𝑍𝑗 ) ) )
26 equequ1 ( 𝑖 = 𝑦 → ( 𝑖 = 𝑗𝑦 = 𝑗 ) )
27 25 26 imbi12d ( 𝑖 = 𝑦 → ( ( ( 𝑍𝑖 ) = ( 𝑍𝑗 ) → 𝑖 = 𝑗 ) ↔ ( ( 𝑍𝑦 ) = ( 𝑍𝑗 ) → 𝑦 = 𝑗 ) ) )
28 fveq2 ( 𝑗 = 𝑧 → ( 𝑍𝑗 ) = ( 𝑍𝑧 ) )
29 28 eqeq2d ( 𝑗 = 𝑧 → ( ( 𝑍𝑦 ) = ( 𝑍𝑗 ) ↔ ( 𝑍𝑦 ) = ( 𝑍𝑧 ) ) )
30 equequ2 ( 𝑗 = 𝑧 → ( 𝑦 = 𝑗𝑦 = 𝑧 ) )
31 29 30 imbi12d ( 𝑗 = 𝑧 → ( ( ( 𝑍𝑦 ) = ( 𝑍𝑗 ) → 𝑦 = 𝑗 ) ↔ ( ( 𝑍𝑦 ) = ( 𝑍𝑧 ) → 𝑦 = 𝑧 ) ) )
32 27 31 rspc2va ( ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑍𝑖 ) = ( 𝑍𝑗 ) → 𝑖 = 𝑗 ) ) → ( ( 𝑍𝑦 ) = ( 𝑍𝑧 ) → 𝑦 = 𝑧 ) )
33 32 expcom ( ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑍𝑖 ) = ( 𝑍𝑗 ) → 𝑖 = 𝑗 ) → ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝑍𝑦 ) = ( 𝑍𝑧 ) → 𝑦 = 𝑧 ) ) )
34 33 a1d ( ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ∀ 𝑗 ∈ ( 𝑁 ∖ { 𝐾 } ) ( ( 𝑍𝑖 ) = ( 𝑍𝑗 ) → 𝑖 = 𝑗 ) → ( 𝐾𝑁 → ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝑍𝑦 ) = ( 𝑍𝑧 ) → 𝑦 = 𝑧 ) ) ) )
35 24 34 simplbiim ( 𝑍 : ( 𝑁 ∖ { 𝐾 } ) –1-1→ ( 𝑁 ∖ { 𝐾 } ) → ( 𝐾𝑁 → ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝑍𝑦 ) = ( 𝑍𝑧 ) → 𝑦 = 𝑧 ) ) ) )
36 22 23 35 3syl ( 𝑍𝑆 → ( 𝐾𝑁 → ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝑍𝑦 ) = ( 𝑍𝑧 ) → 𝑦 = 𝑧 ) ) ) )
37 36 impcom ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝑍𝑦 ) = ( 𝑍𝑧 ) → 𝑦 = 𝑧 ) ) )
38 37 impcom ( ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝐾𝑁𝑍𝑆 ) ) → ( ( 𝑍𝑦 ) = ( 𝑍𝑧 ) → 𝑦 = 𝑧 ) )
39 20 38 sylbid ( ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝐾𝑁𝑍𝑆 ) ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) )
40 39 ex ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) ) )
41 1 2 symgextf1lem ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑦 ∈ { 𝐾 } ) → ( 𝐸𝑧 ) ≠ ( 𝐸𝑦 ) ) )
42 eqneqall ( ( 𝐸𝑧 ) = ( 𝐸𝑦 ) → ( ( 𝐸𝑧 ) ≠ ( 𝐸𝑦 ) → 𝑦 = 𝑧 ) )
43 42 eqcoms ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → ( ( 𝐸𝑧 ) ≠ ( 𝐸𝑦 ) → 𝑦 = 𝑧 ) )
44 43 com12 ( ( 𝐸𝑧 ) ≠ ( 𝐸𝑦 ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) )
45 41 44 syl6com ( ( 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑦 ∈ { 𝐾 } ) → ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) ) )
46 45 ancoms ( ( 𝑦 ∈ { 𝐾 } ∧ 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) ) )
47 1 2 symgextf1lem ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ { 𝐾 } ) → ( 𝐸𝑦 ) ≠ ( 𝐸𝑧 ) ) )
48 eqneqall ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → ( ( 𝐸𝑦 ) ≠ ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) )
49 48 com12 ( ( 𝐸𝑦 ) ≠ ( 𝐸𝑧 ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) )
50 47 49 syl6com ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑧 ∈ { 𝐾 } ) → ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) ) )
51 elsni ( 𝑦 ∈ { 𝐾 } → 𝑦 = 𝐾 )
52 elsni ( 𝑧 ∈ { 𝐾 } → 𝑧 = 𝐾 )
53 eqtr3 ( ( 𝑦 = 𝐾𝑧 = 𝐾 ) → 𝑦 = 𝑧 )
54 53 2a1d ( ( 𝑦 = 𝐾𝑧 = 𝐾 ) → ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) ) )
55 51 52 54 syl2an ( ( 𝑦 ∈ { 𝐾 } ∧ 𝑧 ∈ { 𝐾 } ) → ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) ) )
56 40 46 50 55 ccase ( ( ( 𝑦 ∈ ( 𝑁 ∖ { 𝐾 } ) ∨ 𝑦 ∈ { 𝐾 } ) ∧ ( 𝑧 ∈ ( 𝑁 ∖ { 𝐾 } ) ∨ 𝑧 ∈ { 𝐾 } ) ) → ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) ) )
57 10 11 56 syl2anb ( ( 𝑦 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∧ 𝑧 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) → ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) ) )
58 57 com12 ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝑦 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ∧ 𝑧 ∈ ( ( 𝑁 ∖ { 𝐾 } ) ∪ { 𝐾 } ) ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) ) )
59 9 58 sylbid ( ( 𝐾𝑁𝑍𝑆 ) → ( ( 𝑦𝑁𝑧𝑁 ) → ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) ) )
60 59 ralrimivv ( ( 𝐾𝑁𝑍𝑆 ) → ∀ 𝑦𝑁𝑧𝑁 ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) )
61 dff13 ( 𝐸 : 𝑁1-1𝑁 ↔ ( 𝐸 : 𝑁𝑁 ∧ ∀ 𝑦𝑁𝑧𝑁 ( ( 𝐸𝑦 ) = ( 𝐸𝑧 ) → 𝑦 = 𝑧 ) ) )
62 3 60 61 sylanbrc ( ( 𝐾𝑁𝑍𝑆 ) → 𝐸 : 𝑁1-1𝑁 )