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