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