Metamath Proof Explorer


Theorem symgextf1lem

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

Ref Expression
Hypotheses symgext.s S = Base SymGrp N K
symgext.e E = x N if x = K K Z x
Assertion symgextf1lem K N Z S X N K Y K E X E Y

Proof

Step Hyp Ref Expression
1 symgext.s S = Base SymGrp N K
2 symgext.e E = x N if x = K K Z x
3 eqid SymGrp N K = SymGrp N K
4 3 1 symgfv Z S X N K Z X N K
5 4 adantll K N Z S X N K Z X N K
6 eldifsni Z X N K Z X K
7 1 2 symgextfv K N Z S X N K E X = Z X
8 7 imp K N Z S X N K E X = Z X
9 8 neeq1d K N Z S X N K E X K Z X K
10 6 9 syl5ibr K N Z S X N K Z X N K E X K
11 5 10 mpd K N Z S X N K E X K
12 11 adantrr K N Z S X N K Y K E X K
13 elsni Y K Y = K
14 1 2 symgextfve K N Y = K E Y = K
15 14 adantr K N Z S Y = K E Y = K
16 13 15 syl5com Y K K N Z S E Y = K
17 16 adantl X N K Y K K N Z S E Y = K
18 17 impcom K N Z S X N K Y K E Y = K
19 12 18 neeqtrrd K N Z S X N K Y K E X E Y
20 19 ex K N Z S X N K Y K E X E Y