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

Metamath Proof Explorer

Theorem symgfixfolem1

Description: Lemma 1 for symgfixfo . (Contributed by AV, 7-Jan-2019)

Ref Expression
Hypotheses symgfixf.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
symgfixf.q ⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
symgfixf.s ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
symgfixf.h ⊢ 𝐻 = ( 𝑞 ∈ 𝑄 ↦ ( 𝑞 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
symgfixfo.e ⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
Assertion symgfixfolem1 ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 ∈ 𝑄 )

Proof

Step Hyp Ref Expression
1 symgfixf.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2 symgfixf.q ⊢ 𝑄 = { 𝑞 ∈ 𝑃 ∣ ( 𝑞 ‘ 𝐾 ) = 𝐾 }
3 symgfixf.s ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
4 symgfixf.h ⊢ 𝐻 = ( 𝑞 ∈ 𝑄 ↦ ( 𝑞 ↾ ( 𝑁 ∖ { 𝐾 } ) ) )
5 symgfixfo.e ⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
6 3 5 symgextf1o ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 –1-1-onto→ 𝑁 )
7 6 3adant1 ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 : 𝑁 –1-1-onto→ 𝑁 )
8 iftrue ⊢ ( 𝑥 = 𝐾 → if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) = 𝐾 )
9 simp2 ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐾 ∈ 𝑁 )
10 5 8 9 9 fvmptd3 ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝐸 ‘ 𝐾 ) = 𝐾 )
11 mptexg ⊢ ( 𝑁 ∈ 𝑉 → ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) ) ∈ V )
12 11 3ad2ant1 ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) ) ∈ V )
13 5 12 eqeltrid ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 ∈ V )
14 1 2 symgfixelq ⊢ ( 𝐸 ∈ V → ( 𝐸 ∈ 𝑄 ↔ ( 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐸 ‘ 𝐾 ) = 𝐾 ) ) )
15 13 14 syl ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝐸 ∈ 𝑄 ↔ ( 𝐸 : 𝑁 –1-1-onto→ 𝑁 ∧ ( 𝐸 ‘ 𝐾 ) = 𝐾 ) ) )
16 7 10 15 mpbir2and ⊢ ( ( 𝑁 ∈ 𝑉 ∧ 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → 𝐸 ∈ 𝑄 )