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→ 𝑁 )