symgmatr01lem

		Ref	Expression
	Hypothesis	symgmatr01.p	$⊢ P = {Base}_{SymGrp (N)}$
	Assertion	symgmatr01lem	$⊢ (K \in N \land L \in N) \to (Q \in (P ∖ \{q \in P \| q (K) = L\}) \to \exists k \in N if (k = K, if (Q (k) = L, A, B), k M Q (k)) = B)$

Proof

Step	Hyp	Ref	Expression
1		symgmatr01.p	$⊢ P = {Base}_{SymGrp (N)}$
2		simpll	$⊢ ((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \to K \in N$
3		eqeq1	$⊢ k = K \to (k = K \leftrightarrow K = K)$
4		fveq2	$⊢ k = K \to Q (k) = Q (K)$
5	4	eqeq1d	$⊢ k = K \to (Q (k) = L \leftrightarrow Q (K) = L)$
6	5	ifbid	$⊢ k = K \to if (Q (k) = L, A, B) = if (Q (K) = L, A, B)$
7		id	$⊢ k = K \to k = K$
8	7 4	oveq12d	$⊢ k = K \to k M Q (k) = K M Q (K)$
9	3 6 8	ifbieq12d	$⊢ k = K \to if (k = K, if (Q (k) = L, A, B), k M Q (k)) = if (K = K, if (Q (K) = L, A, B), K M Q (K))$
10	9	eqeq1d	$⊢ k = K \to (if (k = K, if (Q (k) = L, A, B), k M Q (k)) = B \leftrightarrow if (K = K, if (Q (K) = L, A, B), K M Q (K)) = B)$
11	10	adantl	$⊢ (((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \land k = K) \to (if (k = K, if (Q (k) = L, A, B), k M Q (k)) = B \leftrightarrow if (K = K, if (Q (K) = L, A, B), K M Q (K)) = B)$
12		eqidd	$⊢ ((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \to K = K$
13	12	iftrued	$⊢ ((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \to if (K = K, if (Q (K) = L, A, B), K M Q (K)) = if (Q (K) = L, A, B)$
14		eldif	$⊢ Q \in (P ∖ \{q \in P \| q (K) = L\}) \leftrightarrow (Q \in P \land \neg Q \in \{q \in P \| q (K) = L\})$
15		ianor	$⊢ \neg (Q \in P \land Q (K) = L) \leftrightarrow (\neg Q \in P \lor \neg Q (K) = L)$
16		fveq1	$⊢ q = Q \to q (K) = Q (K)$
17	16	eqeq1d	$⊢ q = Q \to (q (K) = L \leftrightarrow Q (K) = L)$
18	17	elrab	$⊢ Q \in \{q \in P \| q (K) = L\} \leftrightarrow (Q \in P \land Q (K) = L)$
19	15 18	xchnxbir	$⊢ \neg Q \in \{q \in P \| q (K) = L\} \leftrightarrow (\neg Q \in P \lor \neg Q (K) = L)$
20		pm2.21	$⊢ \neg Q \in P \to (Q \in P \to \neg Q (K) = L)$
21		ax-1	$⊢ \neg Q (K) = L \to (Q \in P \to \neg Q (K) = L)$
22	20 21	jaoi	$⊢ (\neg Q \in P \lor \neg Q (K) = L) \to (Q \in P \to \neg Q (K) = L)$
23	19 22	sylbi	$⊢ \neg Q \in \{q \in P \| q (K) = L\} \to (Q \in P \to \neg Q (K) = L)$
24	23	impcom	$⊢ (Q \in P \land \neg Q \in \{q \in P \| q (K) = L\}) \to \neg Q (K) = L$
25	14 24	sylbi	$⊢ Q \in (P ∖ \{q \in P \| q (K) = L\}) \to \neg Q (K) = L$
26	25	adantl	$⊢ ((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \to \neg Q (K) = L$
27	26	iffalsed	$⊢ ((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \to if (Q (K) = L, A, B) = B$
28	13 27	eqtrd	$⊢ ((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \to if (K = K, if (Q (K) = L, A, B), K M Q (K)) = B$
29	2 11 28	rspcedvd	$⊢ ((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \to \exists k \in N if (k = K, if (Q (k) = L, A, B), k M Q (k)) = B$
30	29	ex	$⊢ (K \in N \land L \in N) \to (Q \in (P ∖ \{q \in P \| q (K) = L\}) \to \exists k \in N if (k = K, if (Q (k) = L, A, B), k M Q (k)) = B)$

Metamath Proof Explorer

Theorem symgmatr01lem

Proof