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