symgmatr01

Description: Applying a permutation that does not fix a certain element of a set to a second element to an index of a matrix a row with 0's and a 1. (Contributed by AV, 3-Jan-2019)

	Ref	Expression
Hypotheses	symgmatr01.p	$⊢ P = {Base}_{SymGrp (N)}$
	symgmatr01.0	$⊢ \underset{˙}{0} = 0_{R}$
	symgmatr01.1	$⊢ \underset{˙}{1} = 1_{R}$
Assertion	symgmatr01	$⊢ (K \in N \land L \in N) \to (Q \in (P ∖ \{q \in P \| q (K) = L\}) \to \exists k \in N k (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) Q (k) = \underset{˙}{0})$

Proof

Step	Hyp	Ref	Expression
1		symgmatr01.p	$⊢ P = {Base}_{SymGrp (N)}$
2		symgmatr01.0	$⊢ \underset{˙}{0} = 0_{R}$
3		symgmatr01.1	$⊢ \underset{˙}{1} = 1_{R}$
4	1	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, \underset{˙}{1}, \underset{˙}{0}), k M Q (k)) = \underset{˙}{0})$
5	4	imp	$⊢ ((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, \underset{˙}{1}, \underset{˙}{0}), k M Q (k)) = \underset{˙}{0}$
6		eqidd	$⊢ (((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \land k \in N) \to (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) = (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j))$
7		eqeq1	$⊢ i = k \to (i = K \leftrightarrow k = K)$
8	7	adantr	$⊢ (i = k \land j = Q (k)) \to (i = K \leftrightarrow k = K)$
9		eqeq1	$⊢ j = Q (k) \to (j = L \leftrightarrow Q (k) = L)$
10	9	adantl	$⊢ (i = k \land j = Q (k)) \to (j = L \leftrightarrow Q (k) = L)$
11	10	ifbid	$⊢ (i = k \land j = Q (k)) \to if (j = L, \underset{˙}{1}, \underset{˙}{0}) = if (Q (k) = L, \underset{˙}{1}, \underset{˙}{0})$
12		oveq12	$⊢ (i = k \land j = Q (k)) \to i M j = k M Q (k)$
13	8 11 12	ifbieq12d	$⊢ (i = k \land j = Q (k)) \to if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j) = if (k = K, if (Q (k) = L, \underset{˙}{1}, \underset{˙}{0}), k M Q (k))$
14	13	adantl	$⊢ ((((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \land k \in N) \land (i = k \land j = Q (k))) \to if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j) = if (k = K, if (Q (k) = L, \underset{˙}{1}, \underset{˙}{0}), k M Q (k))$
15		simpr	$⊢ (((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \land k \in N) \to k \in N$
16		eldifi	$⊢ Q \in (P ∖ \{q \in P \| q (K) = L\}) \to Q \in P$
17		eqid	$⊢ SymGrp (N) = SymGrp (N)$
18	17 1	symgfv	$⊢ (Q \in P \land k \in N) \to Q (k) \in N$
19	18	ex	$⊢ Q \in P \to (k \in N \to Q (k) \in N)$
20	16 19	syl	$⊢ Q \in (P ∖ \{q \in P \| q (K) = L\}) \to (k \in N \to Q (k) \in N)$
21	20	adantl	$⊢ ((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \to (k \in N \to Q (k) \in N)$
22	21	imp	$⊢ (((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \land k \in N) \to Q (k) \in N$
23	3	fvexi	$⊢ \underset{˙}{1} \in V$
24	2	fvexi	$⊢ \underset{˙}{0} \in V$
25	23 24	ifex	$⊢ if (Q (k) = L, \underset{˙}{1}, \underset{˙}{0}) \in V$
26		ovex	$⊢ k M Q (k) \in V$
27	25 26	ifex	$⊢ if (k = K, if (Q (k) = L, \underset{˙}{1}, \underset{˙}{0}), k M Q (k)) \in V$
28	27	a1i	$⊢ (((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \land k \in N) \to if (k = K, if (Q (k) = L, \underset{˙}{1}, \underset{˙}{0}), k M Q (k)) \in V$
29	6 14 15 22 28	ovmpod	$⊢ (((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \land k \in N) \to k (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) Q (k) = if (k = K, if (Q (k) = L, \underset{˙}{1}, \underset{˙}{0}), k M Q (k))$
30	29	eqeq1d	$⊢ (((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \land k \in N) \to (k (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) Q (k) = \underset{˙}{0} \leftrightarrow if (k = K, if (Q (k) = L, \underset{˙}{1}, \underset{˙}{0}), k M Q (k)) = \underset{˙}{0})$
31	30	rexbidva	$⊢ ((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \to (\exists k \in N k (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) Q (k) = \underset{˙}{0} \leftrightarrow \exists k \in N if (k = K, if (Q (k) = L, \underset{˙}{1}, \underset{˙}{0}), k M Q (k)) = \underset{˙}{0})$
32	5 31	mpbird	$⊢ ((K \in N \land L \in N) \land Q \in (P ∖ \{q \in P \| q (K) = L\})) \to \exists k \in N k (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) Q (k) = \underset{˙}{0}$
33	32	ex	$⊢ (K \in N \land L \in N) \to (Q \in (P ∖ \{q \in P \| q (K) = L\}) \to \exists k \in N k (i \in N, j \in N ⟼ if (i = K, if (j = L, \underset{˙}{1}, \underset{˙}{0}), i M j)) Q (k) = \underset{˙}{0})$

Metamath Proof Explorer

Theorem symgmatr01

Proof