Theorem m2detleiblem6

Description: Lemma 6 for m2detleib . (Contributed by AV, 20-Dec-2018)

	Ref	Expression
Hypotheses	m2detleiblem1.n	⊢ 𝑁 = { 1 , 2 }
	m2detleiblem1.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
	m2detleiblem1.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
	m2detleiblem1.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
	m2detleiblem1.o	⊢ 1 = ( 1r ‘ 𝑅 )
	m2detleiblem1.i	⊢ 𝐼 = ( invg ‘ 𝑅 )
Assertion	m2detleiblem6	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) = ( 𝐼 ‘ 1 ) )

Proof

Step	Hyp	Ref	Expression
1		m2detleiblem1.n	⊢ 𝑁 = { 1 , 2 }
2		m2detleiblem1.p	⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
3		m2detleiblem1.y	⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
4		m2detleiblem1.s	⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
5		m2detleiblem1.o	⊢ 1 = ( 1r ‘ 𝑅 )
6		m2detleiblem1.i	⊢ 𝐼 = ( invg ‘ 𝑅 )
7		1ex	⊢ 1 ∈ V
8		2nn	⊢ 2 ∈ ℕ
9		prex	⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ V
10	9	prid2	⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
11		eqid	⊢ ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
12	11 2 1	symg2bas	⊢ ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → 𝑃 = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
13	10 12	eleqtrrid	⊢ ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃 )
14	7 8 13	mp2an	⊢ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃
15		eleq1	⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑄 ∈ 𝑃 ↔ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ∈ 𝑃 ) )
16	14 15	mpbiri	⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → 𝑄 ∈ 𝑃 )
17	1 2 3 4 5	m2detleiblem1	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) = ( ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) ( .g ‘ 𝑅 ) 1 ) )
18	16 17	sylan2	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) = ( ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) ( .g ‘ 𝑅 ) 1 ) )
19		fveq2	⊢ ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) = ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) )
20	19	adantl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) → ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) = ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) )
21		eqid	⊢ ran ( pmTrsp ‘ 𝑁 ) = ran ( pmTrsp ‘ 𝑁 )
22		eqid	⊢ ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
23	1 11 2 21 22	psgnprfval2	⊢ ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) = - 1
24	20 23	eqtrdi	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) → ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) = - 1 )
25	24	oveq1d	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) → ( ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) ( .g ‘ 𝑅 ) 1 ) = ( - 1 ( .g ‘ 𝑅 ) 1 ) )
26		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
27		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
28	27 5	ringidcl	⊢ ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
29		eqid	⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
30	27 29 6	mulgm1	⊢ ( ( 𝑅 ∈ Grp ∧ 1 ∈ ( Base ‘ 𝑅 ) ) → ( - 1 ( .g ‘ 𝑅 ) 1 ) = ( 𝐼 ‘ 1 ) )
31	26 28 30	syl2anc	⊢ ( 𝑅 ∈ Ring → ( - 1 ( .g ‘ 𝑅 ) 1 ) = ( 𝐼 ‘ 1 ) )
32	31	adantr	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) → ( - 1 ( .g ‘ 𝑅 ) 1 ) = ( 𝐼 ‘ 1 ) )
33	18 25 32	3eqtrd	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) → ( 𝑌 ‘ ( 𝑆 ‘ 𝑄 ) ) = ( 𝐼 ‘ 1 ) )