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	⊢ ( ( 𝐾 ∈ 𝑁 ∧ 𝑍 ∈ 𝑆 ) → ( ( 𝑋 ∈ ( 𝑁 ∖ { 𝐾 } ) ∧ 𝑌 ∈ { 𝐾 } ) → ( 𝐸 ‘ 𝑋 ) ≠ ( 𝐸 ‘ 𝑌 ) ) )