# Metamath Proof Explorer

## 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 ) )