Theorem m2detleiblem1

Description: Lemma 1 for m2detleib . (Contributed by AV, 12-Dec-2018)

	Ref	Expression
Hypotheses	m2detleiblem1.n	$$⊢N=\left\{1,2\right\}$$
	m2detleiblem1.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
	m2detleiblem1.y	$$⊢Y=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	m2detleiblem1.s	$$⊢S=\mathrm{pmSgn}\left(N\right)$$
	m2detleiblem1.o	$$⊢\underset{\dot{}}{1}=1_R$$
Assertion	m2detleiblem1	$$⊢\left(R\in \mathrm{Ring}\wedge Q\in P\right)\to Y\left(S\left(Q\right)\right)=\mathrm{pmSgn}\left(N\right)\left(Q\right){\cdot }_R\underset{\dot{}}{1}$$

Proof

Step	Hyp	Ref	Expression
1		m2detleiblem1.n	$$⊢N=\left\{1,2\right\}$$
2		m2detleiblem1.p	$$⊢P={\mathrm{Base}}_{\mathrm{SymGrp}\left(N\right)}$$
3		m2detleiblem1.y	$$⊢Y=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
4		m2detleiblem1.s	$$⊢S=\mathrm{pmSgn}\left(N\right)$$
5		m2detleiblem1.o	$$⊢\underset{\dot{}}{1}=1_R$$
6		elpri	$$⊢Q\in \left\{\left\{⟨1,1⟩,⟨2,2⟩\right\},\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}\to \left(Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\vee Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)$$
7		fveq2	$$⊢Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\to S\left(Q\right)=S\left(\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)$$
8		eqid	$$⊢\mathrm{SymGrp}\left(N\right)=\mathrm{SymGrp}\left(N\right)$$
9		eqid	$$⊢\mathrm{ran}\mathrm{pmTrsp}\left(N\right)=\mathrm{ran}\mathrm{pmTrsp}\left(N\right)$$
10	1 8 2 9 4	psgnprfval1	$$⊢S\left(\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)=1$$
11	7 10	eqtrdi	$$⊢Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\to S\left(Q\right)=1$$
12		1z	$$⊢1\in \mathbb{Z}$$
13	11 12	eqeltrdi	$$⊢Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\to S\left(Q\right)\in \mathbb{Z}$$
14		fveq2	$$⊢Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\to S\left(Q\right)=S\left(\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)$$
15	1 8 2 9 4	psgnprfval2	$$⊢S\left(\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)=-1$$
16	14 15	eqtrdi	$$⊢Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\to S\left(Q\right)=-1$$
17		neg1z	$$⊢-1\in \mathbb{Z}$$
18	16 17	eqeltrdi	$$⊢Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\to S\left(Q\right)\in \mathbb{Z}$$
19	13 18	jaoi	$$⊢\left(Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\vee Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)\to S\left(Q\right)\in \mathbb{Z}$$
20	6 19	syl	$$⊢Q\in \left\{\left\{⟨1,1⟩,⟨2,2⟩\right\},\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}\to S\left(Q\right)\in \mathbb{Z}$$
21		1ex	$$⊢1\in \mathrm{V}$$
22		2nn	$$⊢2\in \mathbb{N}$$
23	8 2 1	symg2bas	$$⊢\left(1\in \mathrm{V}\wedge 2\in \mathbb{N}\right)\to P=\left\{\left\{⟨1,1⟩,⟨2,2⟩\right\},\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
24	21 22 23	mp2an	$$⊢P=\left\{\left\{⟨1,1⟩,⟨2,2⟩\right\},\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
25	20 24	eleq2s	$$⊢Q\in P\to S\left(Q\right)\in \mathbb{Z}$$
26		eqid	$$⊢{\cdot }_R={\cdot }_R$$
27	3 26 5	zrhmulg	$$⊢\left(R\in \mathrm{Ring}\wedge S\left(Q\right)\in \mathbb{Z}\right)\to Y\left(S\left(Q\right)\right)=S\left(Q\right){\cdot }_R\underset{\dot{}}{1}$$
28	25 27	sylan2	$$⊢\left(R\in \mathrm{Ring}\wedge Q\in P\right)\to Y\left(S\left(Q\right)\right)=S\left(Q\right){\cdot }_R\underset{\dot{}}{1}$$
29	4	a1i	$$⊢\left(R\in \mathrm{Ring}\wedge Q\in P\right)\to S=\mathrm{pmSgn}\left(N\right)$$
30	29	fveq1d	$$⊢\left(R\in \mathrm{Ring}\wedge Q\in P\right)\to S\left(Q\right)=\mathrm{pmSgn}\left(N\right)\left(Q\right)$$
31	30	oveq1d	$$⊢\left(R\in \mathrm{Ring}\wedge Q\in P\right)\to S\left(Q\right){\cdot }_R\underset{\dot{}}{1}=\mathrm{pmSgn}\left(N\right)\left(Q\right){\cdot }_R\underset{\dot{}}{1}$$
32	28 31	eqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge Q\in P\right)\to Y\left(S\left(Q\right)\right)=\mathrm{pmSgn}\left(N\right)\left(Q\right){\cdot }_R\underset{\dot{}}{1}$$