This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem symgextres

Description: The restriction of the extension of a permutation, fixing the additional element, to the original domain. (Contributed by AV, 6-Jan-2019)

Ref Expression
Hypotheses symgext.s ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
symgext.e ⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
Assertion symgextres ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝐸 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = 𝑍 )

Proof

Step Hyp Ref Expression
1 symgext.s ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
2 symgext.e ⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
3 1 2 symgextfv ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝐸 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) )
4 3 ralrimiv ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝐸 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) )
5 1 2 symgextf ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 ⟶ 𝑁 )
6 5 ffnd ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 Fn 𝑁 )
7 eqid ⊢ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
8 7 1 symgbasf ⊢ ( 𝑍 ∈ 𝑆 → 𝑍 : ( 𝑁 ∖ { 𝐾 } ) ⟶ ( 𝑁 ∖ { 𝐾 } ) )
9 8 ffnd ⊢ ( 𝑍 ∈ 𝑆 → 𝑍 Fn ( 𝑁 ∖ { 𝐾 } ) )
10 9 adantl ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝑍 Fn ( 𝑁 ∖ { 𝐾 } ) )
11 difssd ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 )
12 fvreseq1 ⊢ ( ( ( 𝐸 Fn 𝑁 ∧ 𝑍 Fn ( 𝑁 ∖ { 𝐾 } ) ) ∧ ( 𝑁 ∖ { 𝐾 } ) ⊆ 𝑁 ) → ( ( 𝐸 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = 𝑍 ↔ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝐸 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) )
13 6 10 11 12 syl21anc ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( ( 𝐸 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = 𝑍 ↔ ∀ 𝑖 ∈ ( 𝑁 ∖ { 𝐾 } ) ( 𝐸 ‘ 𝑖 ) = ( 𝑍 ‘ 𝑖 ) ) )
14 4 13 mpbird ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝐸 ↾ ( 𝑁 ∖ { 𝐾 } ) ) = 𝑍 )