Metamath Proof Explorer

Theorem madetsmelbas2

Description: A summand of the determinant of a matrix belongs to the underlying ring. (Contributed by AV, 1-Jan-2019)

Ref Expression
Hypotheses madetsmelbas.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
madetsmelbas.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
madetsmelbas.y ⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
madetsmelbas.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
madetsmelbas.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
madetsmelbas.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
Assertion madetsmelbas2 ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 𝑀 ( 𝑄 ‘ 𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )

Proof

Step Hyp Ref Expression
1 madetsmelbas.p ⊢ 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
2 madetsmelbas.s ⊢ 𝑆 = ( pmSgn ‘ 𝑁 )
3 madetsmelbas.y ⊢ 𝑌 = ( ℤRHom ‘ 𝑅 )
4 madetsmelbas.a ⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
5 madetsmelbas.b ⊢ 𝐵 = ( Base ‘ 𝐴 )
6 madetsmelbas.g ⊢ 𝐺 = ( mulGrp ‘ 𝑅 )
7 crngring ⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
8 7 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃 ) → 𝑅 ∈ Ring )
9 4 5 matrcl ⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
10 9 simpld ⊢ ( 𝑀 ∈ 𝐵 → 𝑁 ∈ Fin )
11 10 3ad2ant2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃 ) → 𝑁 ∈ Fin )
12 simp3 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃 ) → 𝑄 ∈ 𝑃 )
13 1 2 3 zrhcopsgnelbas ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ∧ 𝑄 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) ∈ ( Base ‘ 𝑅 ) )
14 8 11 12 13 syl3anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃 ) → ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) ∈ ( Base ‘ 𝑅 ) )
15 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
16 6 15 mgpbas ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝐺 )
17 6 crngmgp ⊢ ( 𝑅 ∈ CRing → 𝐺 ∈ CMnd )
18 17 3ad2ant1 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃 ) → 𝐺 ∈ CMnd )
19 simp2 ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃 ) → 𝑀 ∈ 𝐵 )
20 4 5 1 matepm2cl ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑄 ∈ 𝑃 ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝑅 ) )
21 8 12 19 20 syl3anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃 ) → ∀ 𝑛 ∈ 𝑁 ( 𝑛 𝑀 ( 𝑄 ‘ 𝑛 ) ) ∈ ( Base ‘ 𝑅 ) )
22 16 18 11 21 gsummptcl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃 ) → ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 𝑀 ( 𝑄 ‘ 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
23 eqid ⊢ ( .r ‘ 𝑅 ) = ( .r ‘ 𝑅 )
24 15 23 ringcl ⊢ ( ( 𝑅 ∈ Ring ∧ ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) ∈ ( Base ‘ 𝑅 ) ∧ ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 𝑀 ( 𝑄 ‘ 𝑛 ) ) ) ) ∈ ( Base ‘ 𝑅 ) ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 𝑀 ( 𝑄 ‘ 𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )
25 8 14 22 24 syl3anc ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ∧ 𝑄 ∈ 𝑃 ) → ( ( ( 𝑌 ∘ 𝑆 ) ‘ 𝑄 ) ( .r ‘ 𝑅 ) ( 𝐺 Σg ( 𝑛 ∈ 𝑁 ↦ ( 𝑛 𝑀 ( 𝑄 ‘ 𝑛 ) ) ) ) ) ∈ ( Base ‘ 𝑅 ) )