Theorem 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={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
	symgmatr01.0	$$⊢\underset{\dot{}}{0}=0_R$$
	symgmatr01.1	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	symgmatr01	$$⊢\left(K\in N\wedge L\in N\right)\to \left(Q\in \left(P\setminus \left\{q\in P|q\left(K\right)=L\right\}\right)\to \exists k\in Nk\left(i\in N,j\in N⟼if\left(i=K,if\left(j=L,\underset{\dot{}}{1},\underset{\dot{}}{0}\right),iMj\right)\right)Q\left(k\right)=\underset{\dot{}}{0}\right)$$

Proof

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