Metamath Proof Explorer

Theorem m2detleiblem5

Description: Lemma 5 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𝑅 )
Assertion m2detleiblem5 ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) → ( 𝑌 ‘ ( 𝑆𝑄 ) ) = 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 1ex 1 ∈ V
7 2nn 2 ∈ ℕ
8 prex { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ V
9 8 prid1 { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } }
10 eqid ( SymGrp ‘ 𝑁 ) = ( SymGrp ‘ 𝑁 )
11 10 2 1 symg2bas ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → 𝑃 = { { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } , { ⟨ 1 , 2 ⟩ , ⟨ 2 , 1 ⟩ } } )
12 9 11 eleqtrrid ( ( 1 ∈ V ∧ 2 ∈ ℕ ) → { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ 𝑃 )
13 6 7 12 mp2an { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ 𝑃
14 eleq1 ( 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( 𝑄𝑃 ↔ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ∈ 𝑃 ) )
15 13 14 mpbiri ( 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → 𝑄𝑃 )
16 1 2 3 4 5 m2detleiblem1 ( ( 𝑅 ∈ Ring ∧ 𝑄𝑃 ) → ( 𝑌 ‘ ( 𝑆𝑄 ) ) = ( ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) ( .g𝑅 ) 1 ) )
17 15 16 sylan2 ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) → ( 𝑌 ‘ ( 𝑆𝑄 ) ) = ( ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) ( .g𝑅 ) 1 ) )
18 fveq2 ( 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } → ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) = ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) )
19 18 adantl ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) → ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) = ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) )
20 eqid ran ( pmTrsp ‘ 𝑁 ) = ran ( pmTrsp ‘ 𝑁 )
21 eqid ( pmSgn ‘ 𝑁 ) = ( pmSgn ‘ 𝑁 )
22 1 10 2 20 21 psgnprfval1 ( ( pmSgn ‘ 𝑁 ) ‘ { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) = 1
23 19 22 eqtrdi ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) → ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) = 1 )
24 23 oveq1d ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) → ( ( ( pmSgn ‘ 𝑁 ) ‘ 𝑄 ) ( .g𝑅 ) 1 ) = ( 1 ( .g𝑅 ) 1 ) )
25 eqid ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
26 25 5 ringidcl ( 𝑅 ∈ Ring → 1 ∈ ( Base ‘ 𝑅 ) )
27 26 adantr ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) → 1 ∈ ( Base ‘ 𝑅 ) )
28 eqid ( .g𝑅 ) = ( .g𝑅 )
29 25 28 mulg1 ( 1 ∈ ( Base ‘ 𝑅 ) → ( 1 ( .g𝑅 ) 1 ) = 1 )
30 27 29 syl ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) → ( 1 ( .g𝑅 ) 1 ) = 1 )
31 17 24 30 3eqtrd ( ( 𝑅 ∈ Ring ∧ 𝑄 = { ⟨ 1 , 1 ⟩ , ⟨ 2 , 2 ⟩ } ) → ( 𝑌 ‘ ( 𝑆𝑄 ) ) = 1 )