Theorem m2detleiblem6

Description: Lemma 6 for m2detleib . (Contributed by AV, 20-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$$
	m2detleiblem1.i	$$⊢I={inv}_g\left(R\right)$$
Assertion	m2detleiblem6	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)\to Y\left(S\left(Q\right)\right)=I\left(\underset{\dot{}}{1}\right)$$

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		m2detleiblem1.i	$$⊢I={inv}_g\left(R\right)$$
7		1ex	$$⊢1\in \mathrm{V}$$
8		2nn	$$⊢2\in \mathbb{N}$$
9		prex	$$⊢\left\{⟨1,2⟩,⟨2,1⟩\right\}\in \mathrm{V}$$
10	9	prid2	$$⊢\left\{⟨1,2⟩,⟨2,1⟩\right\}\in \left\{\left\{⟨1,1⟩,⟨2,2⟩\right\},\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
11		eqid	$$⊢\mathrm{SymGrp}\left(N\right)=\mathrm{SymGrp}\left(N\right)$$
12	11 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\}$$
13	10 12	eleqtrrid	$$⊢\left(1\in \mathrm{V}\wedge 2\in \mathbb{N}\right)\to \left\{⟨1,2⟩,⟨2,1⟩\right\}\in P$$
14	7 8 13	mp2an	$$⊢\left\{⟨1,2⟩,⟨2,1⟩\right\}\in P$$
15		eleq1	$$⊢Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\to \left(Q\in P\leftrightarrow \left\{⟨1,2⟩,⟨2,1⟩\right\}\in P\right)$$
16	14 15	mpbiri	$$⊢Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\to Q\in P$$
17	1 2 3 4 5	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}$$
18	16 17	sylan2	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)\to Y\left(S\left(Q\right)\right)=\mathrm{pmSgn}\left(N\right)\left(Q\right){\cdot }_R\underset{\dot{}}{1}$$
19		fveq2	$$⊢Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\to \mathrm{pmSgn}\left(N\right)\left(Q\right)=\mathrm{pmSgn}\left(N\right)\left(\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)$$
20	19	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)\to \mathrm{pmSgn}\left(N\right)\left(Q\right)=\mathrm{pmSgn}\left(N\right)\left(\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)$$
21		eqid	$$⊢\mathrm{ran}\mathrm{pmTrsp}\left(N\right)=\mathrm{ran}\mathrm{pmTrsp}\left(N\right)$$
22		eqid	$$⊢\mathrm{pmSgn}\left(N\right)=\mathrm{pmSgn}\left(N\right)$$
23	1 11 2 21 22	psgnprfval2	$$⊢\mathrm{pmSgn}\left(N\right)\left(\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)=-1$$
24	20 23	eqtrdi	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)\to \mathrm{pmSgn}\left(N\right)\left(Q\right)=-1$$
25	24	oveq1d	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)\to \mathrm{pmSgn}\left(N\right)\left(Q\right){\cdot }_R\underset{\dot{}}{1}=-1{\cdot }_R\underset{\dot{}}{1}$$
26		ringgrp	$$⊢R\in \mathrm{Ring}\to R\in \mathrm{Grp}$$
27		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
28	27 5	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
29		eqid	$$⊢{\cdot }_R={\cdot }_R$$
30	27 29 6	mulgm1	$$⊢\left(R\in \mathrm{Grp}\wedge \underset{\dot{}}{1}\in {\mathrm{Base}}_R\right)\to -1{\cdot }_R\underset{\dot{}}{1}=I\left(\underset{\dot{}}{1}\right)$$
31	26 28 30	syl2anc	$$⊢R\in \mathrm{Ring}\to -1{\cdot }_R\underset{\dot{}}{1}=I\left(\underset{\dot{}}{1}\right)$$
32	31	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)\to -1{\cdot }_R\underset{\dot{}}{1}=I\left(\underset{\dot{}}{1}\right)$$
33	18 25 32	3eqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,2⟩,⟨2,1⟩\right\}\right)\to Y\left(S\left(Q\right)\right)=I\left(\underset{\dot{}}{1}\right)$$