Theorem m2detleiblem5

Description: Lemma 5 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$$
Assertion	m2detleiblem5	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)\to Y\left(S\left(Q\right)\right)=\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		1ex	$$⊢1\in \mathrm{V}$$
7		2nn	$$⊢2\in \mathbb{N}$$
8		prex	$$⊢\left\{⟨1,1⟩,⟨2,2⟩\right\}\in \mathrm{V}$$
9	8	prid1	$$⊢\left\{⟨1,1⟩,⟨2,2⟩\right\}\in \left\{\left\{⟨1,1⟩,⟨2,2⟩\right\},\left\{⟨1,2⟩,⟨2,1⟩\right\}\right\}$$
10		eqid	$$⊢\mathrm{SymGrp}\left(N\right)=\mathrm{SymGrp}\left(N\right)$$
11	10 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\}$$
12	9 11	eleqtrrid	$$⊢\left(1\in \mathrm{V}\wedge 2\in \mathbb{N}\right)\to \left\{⟨1,1⟩,⟨2,2⟩\right\}\in P$$
13	6 7 12	mp2an	$$⊢\left\{⟨1,1⟩,⟨2,2⟩\right\}\in P$$
14		eleq1	$$⊢Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\to \left(Q\in P\leftrightarrow \left\{⟨1,1⟩,⟨2,2⟩\right\}\in P\right)$$
15	13 14	mpbiri	$$⊢Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\to Q\in P$$
16	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}$$
17	15 16	sylan2	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)\to Y\left(S\left(Q\right)\right)=\mathrm{pmSgn}\left(N\right)\left(Q\right){\cdot }_R\underset{\dot{}}{1}$$
18		fveq2	$$⊢Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\to \mathrm{pmSgn}\left(N\right)\left(Q\right)=\mathrm{pmSgn}\left(N\right)\left(\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)$$
19	18	adantl	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)\to \mathrm{pmSgn}\left(N\right)\left(Q\right)=\mathrm{pmSgn}\left(N\right)\left(\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)$$
20		eqid	$$⊢\mathrm{ran}\mathrm{pmTrsp}\left(N\right)=\mathrm{ran}\mathrm{pmTrsp}\left(N\right)$$
21		eqid	$$⊢\mathrm{pmSgn}\left(N\right)=\mathrm{pmSgn}\left(N\right)$$
22	1 10 2 20 21	psgnprfval1	$$⊢\mathrm{pmSgn}\left(N\right)\left(\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)=1$$
23	19 22	eqtrdi	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)\to \mathrm{pmSgn}\left(N\right)\left(Q\right)=1$$
24	23	oveq1d	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)\to \mathrm{pmSgn}\left(N\right)\left(Q\right){\cdot }_R\underset{\dot{}}{1}=1{\cdot }_R\underset{\dot{}}{1}$$
25		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
26	25 5	ringidcl	$$⊢R\in \mathrm{Ring}\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
27	26	adantr	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)\to \underset{\dot{}}{1}\in {\mathrm{Base}}_R$$
28		eqid	$$⊢{\cdot }_R={\cdot }_R$$
29	25 28	mulg1	$$⊢\underset{\dot{}}{1}\in {\mathrm{Base}}_R\to 1{\cdot }_R\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
30	27 29	syl	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)\to 1{\cdot }_R\underset{\dot{}}{1}=\underset{\dot{}}{1}$$
31	17 24 30	3eqtrd	$$⊢\left(R\in \mathrm{Ring}\wedge Q=\left\{⟨1,1⟩,⟨2,2⟩\right\}\right)\to Y\left(S\left(Q\right)\right)=\underset{\dot{}}{1}$$