# Metamath Proof Explorer

## Theorem m2detleiblem1

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

Ref Expression
Hypotheses m2detleiblem1.n 𝑁 = { 1 , 2 }
m2detleiblem1.p 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
m2detleiblem1.y 𝑌 = ( ℤRHom ‘ 𝑅 )
m2detleiblem1.s 𝑆 = ( pmSgn ‘ 𝑁 )
m2detleiblem1.o 1 = ( 1r𝑅 )
Assertion m2detleiblem1 ( ( 𝑅 ∈ Ring ∧ 𝑄𝑃 ) → ( 𝑌 ‘ ( 𝑆𝑄 ) ) = ( ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) ( .g𝑅 ) 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 elpri ( 𝑄 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } → ( 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∨ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) )
7 fveq2 ( 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( 𝑆𝑄 ) = ( 𝑆 ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) )
8 eqid ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
9 eqid ran ( pmTrsp ‘ 𝑁 ) = ran ( pmTrsp ‘ 𝑁 )
10 1 8 2 9 4 psgnprfval1 ( 𝑆 ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) = 1
11 7 10 eqtrdi ( 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( 𝑆𝑄 ) = 1 )
12 1z 1 ∈ ℤ
13 11 12 eqeltrdi ( 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( 𝑆𝑄 ) ∈ ℤ )
14 fveq2 ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑆𝑄 ) = ( 𝑆 ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) )
15 1 8 2 9 4 psgnprfval2 ( 𝑆 ‘ { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) = - 1
16 14 15 eqtrdi ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑆𝑄 ) = - 1 )
17 neg1z - 1 ∈ ℤ
18 16 17 eqeltrdi ( 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } → ( 𝑆𝑄 ) ∈ ℤ )
19 13 18 jaoi ( ( 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∨ 𝑄 = { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } ) → ( 𝑆𝑄 ) ∈ ℤ )
20 6 19 syl ( 𝑄 ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } → ( 𝑆𝑄 ) ∈ ℤ )
21 1ex 1 ∈ V
22 2nn 2 ∈ ℕ
23 8 2 1 symg2bas ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → 𝑃 = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
24 21 22 23 mp2an 𝑃 = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
25 20 24 eleq2s ( 𝑄𝑃 → ( 𝑆𝑄 ) ∈ ℤ )
26 eqid ( .g𝑅 ) = ( .g𝑅 )
27 3 26 5 zrhmulg ( ( 𝑅 ∈ Ring ∧ ( 𝑆𝑄 ) ∈ ℤ ) → ( 𝑌 ‘ ( 𝑆𝑄 ) ) = ( ( 𝑆𝑄 ) ( .g𝑅 ) 1 ) )
28 25 27 sylan2 ( ( 𝑅 ∈ Ring ∧ 𝑄𝑃 ) → ( 𝑌 ‘ ( 𝑆𝑄 ) ) = ( ( 𝑆𝑄 ) ( .g𝑅 ) 1 ) )
29 4 a1i ( ( 𝑅 ∈ Ring ∧ 𝑄𝑃 ) → 𝑆 = ( pmSgn ‘ 𝑁 ) )
30 29 fveq1d ( ( 𝑅 ∈ Ring ∧ 𝑄𝑃 ) → ( 𝑆𝑄 ) = ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) )
31 30 oveq1d ( ( 𝑅 ∈ Ring ∧ 𝑄𝑃 ) → ( ( 𝑆𝑄 ) ( .g𝑅 ) 1 ) = ( ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) ( .g𝑅 ) 1 ) )
32 28 31 eqtrd ( ( 𝑅 ∈ Ring ∧ 𝑄𝑃 ) → ( 𝑌 ‘ ( 𝑆𝑄 ) ) = ( ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) ( .g𝑅 ) 1 ) )