Metamath Proof Explorer

Theorem symgmatr01lem

Description: Lemma for symgmatr01 . (Contributed by AV, 3-Jan-2019)

Ref Expression
Hypothesis symgmatr01.p ⊢P=BaseSymGrp⁡N
Assertion symgmatr01lem ⊢K∈N∧L∈N→Q∈P∖q∈P|q⁡K=L→∃k∈Nifk=KifQ⁡k=LABkMQ⁡k=B

Proof

Step Hyp Ref Expression
1 symgmatr01.p ⊢P=BaseSymGrp⁡N
2 simpll ⊢K∈N∧L∈N∧Q∈P∖q∈P|q⁡K=L→K∈N
3 eqeq1 ⊢k=K→k=K↔K=K
4 fveq2 ⊢k=K→Q⁡k=Q⁡K
5 4 eqeq1d ⊢k=K→Q⁡k=L↔Q⁡K=L
6 5 ifbid ⊢k=K→ifQ⁡k=LAB=ifQ⁡K=LAB
7 id ⊢k=K→k=K
8 7 4 oveq12d ⊢k=K→kMQ⁡k=KMQ⁡K
9 3 6 8 ifbieq12d ⊢k=K→ifk=KifQ⁡k=LABkMQ⁡k=ifK=KifQ⁡K=LABKMQ⁡K
10 9 eqeq1d ⊢k=K→ifk=KifQ⁡k=LABkMQ⁡k=B↔ifK=KifQ⁡K=LABKMQ⁡K=B
11 10 adantl ⊢K∈N∧L∈N∧Q∈P∖q∈P|q⁡K=L∧k=K→ifk=KifQ⁡k=LABkMQ⁡k=B↔ifK=KifQ⁡K=LABKMQ⁡K=B
12 eqidd ⊢K∈N∧L∈N∧Q∈P∖q∈P|q⁡K=L→K=K
13 12 iftrued ⊢K∈N∧L∈N∧Q∈P∖q∈P|q⁡K=L→ifK=KifQ⁡K=LABKMQ⁡K=ifQ⁡K=LAB
14 eldif ⊢Q∈P∖q∈P|q⁡K=L↔Q∈P∧¬Q∈q∈P|q⁡K=L
15 ianor ⊢¬Q∈P∧Q⁡K=L↔¬Q∈P∨¬Q⁡K=L
16 fveq1 ⊢q=Q→q⁡K=Q⁡K
17 16 eqeq1d ⊢q=Q→q⁡K=L↔Q⁡K=L
18 17 elrab ⊢Q∈q∈P|q⁡K=L↔Q∈P∧Q⁡K=L
19 15 18 xchnxbir ⊢¬Q∈q∈P|q⁡K=L↔¬Q∈P∨¬Q⁡K=L
20 pm2.21 ⊢¬Q∈P→Q∈P→¬Q⁡K=L
21 ax-1 ⊢¬Q⁡K=L→Q∈P→¬Q⁡K=L
22 20 21 jaoi ⊢¬Q∈P∨¬Q⁡K=L→Q∈P→¬Q⁡K=L
23 19 22 sylbi ⊢¬Q∈q∈P|q⁡K=L→Q∈P→¬Q⁡K=L
24 23 impcom ⊢Q∈P∧¬Q∈q∈P|q⁡K=L→¬Q⁡K=L
25 14 24 sylbi ⊢Q∈P∖q∈P|q⁡K=L→¬Q⁡K=L
26 25 adantl ⊢K∈N∧L∈N∧Q∈P∖q∈P|q⁡K=L→¬Q⁡K=L
27 26 iffalsed ⊢K∈N∧L∈N∧Q∈P∖q∈P|q⁡K=L→ifQ⁡K=LAB=B
28 13 27 eqtrd ⊢K∈N∧L∈N∧Q∈P∖q∈P|q⁡K=L→ifK=KifQ⁡K=LABKMQ⁡K=B
29 2 11 28 rspcedvd ⊢K∈N∧L∈N∧Q∈P∖q∈P|q⁡K=L→∃k∈Nifk=KifQ⁡k=LABkMQ⁡k=B
30 29 ex ⊢K∈N∧L∈N→Q∈P∖q∈P|q⁡K=L→∃k∈Nifk=KifQ⁡k=LABkMQ⁡k=B