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

Metamath Proof Explorer

Theorem symgextf1lem

Description: Lemma for symgextf1 . (Contributed by AV, 6-Jan-2019)

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

Proof

Step Hyp Ref Expression
1 symgext.s ⊢ 𝑆 = ( Base ‘ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) )
2 symgext.e ⊢ 𝐸 = ( 𝑥 ∈ 𝑁 ↦ if ( 𝑥 = 𝐾 , 𝐾 , ( 𝑍 ‘ 𝑥 ) ) )
3 eqid ⊢ ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) ) = ( SymGrp ‘ ( 𝑁 ∖ { 𝐾 } ) )
4 3 1 symgfv ⊢ ( ( 𝑍 ∈ 𝑆 ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑍 ‘ 𝑋 ) ∈ ( 𝑁 ∖ { 𝐾 } ) )
5 4 adantll ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝑍 ‘ 𝑋 ) ∈ ( 𝑁 ∖ { 𝐾 } ) )
6 eldifsni ⊢ ( ( 𝑍 ‘ 𝑋 ) ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝑍 ‘ 𝑋 ) ≠ 𝐾 )
7 1 2 symgextfv ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝐸 ‘ 𝑋 ) = ( 𝑍 ‘ 𝑋 ) ) )
8 7 imp ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝐸 ‘ 𝑋 ) = ( 𝑍 ‘ 𝑋 ) )
9 8 neeq1d ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝐸 ‘ 𝑋 ) ≠ 𝐾 ↔ ( 𝑍 ‘ 𝑋 ) ≠ 𝐾 ) )
10 6 9 imbitrrid ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( ( 𝑍 ‘ 𝑋 ) ∈ ( 𝑁 ∖ { 𝐾 } ) → ( 𝐸 ‘ 𝑋 ) ≠ 𝐾 ) )
11 5 10 mpd ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ) → ( 𝐸 ‘ 𝑋 ) ≠ 𝐾 )
12 11 adantrr ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑌 ∈ { 𝐾 } ) ) → ( 𝐸 ‘ 𝑋 ) ≠ 𝐾 )
13 elsni ⊢ ( 𝑌 ∈ { 𝐾 } → 𝑌 = 𝐾 )
14 1 2 symgextfve ⊢ ( 𝐾 ∈ 𝑁 → ( 𝑌 = 𝐾 → ( 𝐸 ‘ 𝑌 ) = 𝐾 ) )
15 14 adantr ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝑌 = 𝐾 → ( 𝐸 ‘ 𝑌 ) = 𝐾 ) )
16 13 15 syl5com ⊢ ( 𝑌 ∈ { 𝐾 } → ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝐸 ‘ 𝑌 ) = 𝐾 ) )
17 16 adantl ⊢ ( ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑌 ∈ { 𝐾 } ) → ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( 𝐸 ‘ 𝑌 ) = 𝐾 ) )
18 17 impcom ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑌 ∈ { 𝐾 } ) ) → ( 𝐸 ‘ 𝑌 ) = 𝐾 )
19 12 18 neeqtrrd ⊢ ( ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) ∧ ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑌 ∈ { 𝐾 } ) ) → ( 𝐸 ‘ 𝑋 ) ≠ ( 𝐸 ‘ 𝑌 ) )
20 19 ex ⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑌 ∈ { 𝐾 } ) → ( 𝐸 ‘ 𝑋 ) ≠ ( 𝐸 ‘ 𝑌 ) ) )