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 )