Metamath Proof Explorer


Theorem smadiadetlem0

Description: Lemma 0 for smadiadet : The products of the Leibniz' formula vanish for all permutations fixing the index of the row containing the 0's and the 1 to the column with the 1. (Contributed by AV, 3-Jan-2019)

Ref Expression
Hypotheses marep01ma.a 𝐴 = ( 𝑁 Mat 𝑅 )
marep01ma.b 𝐵 = ( Base ‘ 𝐴 )
marep01ma.r 𝑅 ∈ CRing
marep01ma.0 0 = ( 0g𝑅 )
marep01ma.1 1 = ( 1r𝑅 )
smadiadetlem.p 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
smadiadetlem.g 𝐺 = ( mulGrp ‘ 𝑅 )
Assertion smadiadetlem0 ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) → ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) → ( 𝐺 Σg ( 𝑛𝑁 ↦ ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑛 ) ) ) ) = 0 ) )

Proof

Step Hyp Ref Expression
1 marep01ma.a 𝐴 = ( 𝑁 Mat 𝑅 )
2 marep01ma.b 𝐵 = ( Base ‘ 𝐴 )
3 marep01ma.r 𝑅 ∈ CRing
4 marep01ma.0 0 = ( 0g𝑅 )
5 marep01ma.1 1 = ( 1r𝑅 )
6 smadiadetlem.p 𝑃 = ( Base ‘ ( SymGrp ‘ 𝑁 ) )
7 smadiadetlem.g 𝐺 = ( mulGrp ‘ 𝑅 )
8 3 a1i ( ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) ) → 𝑅 ∈ CRing )
9 1 2 matrcl ( 𝑀𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
10 9 simpld ( 𝑀𝐵𝑁 ∈ Fin )
11 10 3ad2ant1 ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) → 𝑁 ∈ Fin )
12 11 adantr ( ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) ) → 𝑁 ∈ Fin )
13 crngring ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
14 3 13 mp1i ( ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) ) → 𝑅 ∈ Ring )
15 eldifi ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) → 𝑄𝑃 )
16 15 adantl ( ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) ) → 𝑄𝑃 )
17 1 2 3 4 5 marep01ma ( 𝑀𝐵 → ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ∈ 𝐵 )
18 17 3ad2ant1 ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ∈ 𝐵 )
19 18 adantr ( ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) ) → ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ∈ 𝐵 )
20 1 2 6 matepm2cl ( ( 𝑅 ∈ Ring ∧ 𝑄𝑃 ∧ ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ∈ 𝐵 ) → ∀ 𝑚𝑁 ( 𝑚 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑚 ) ) ∈ ( Base ‘ 𝑅 ) )
21 14 16 19 20 syl3anc ( ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) ) → ∀ 𝑚𝑁 ( 𝑚 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑚 ) ) ∈ ( Base ‘ 𝑅 ) )
22 id ( 𝑚 = 𝑛𝑚 = 𝑛 )
23 fveq2 ( 𝑚 = 𝑛 → ( 𝑄𝑚 ) = ( 𝑄𝑛 ) )
24 22 23 oveq12d ( 𝑚 = 𝑛 → ( 𝑚 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑚 ) ) = ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑛 ) ) )
25 24 eleq1d ( 𝑚 = 𝑛 → ( ( 𝑚 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑚 ) ) ∈ ( Base ‘ 𝑅 ) ↔ ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝑅 ) ) )
26 25 rspccv ( ∀ 𝑚𝑁 ( 𝑚 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑚 ) ) ∈ ( Base ‘ 𝑅 ) → ( 𝑛𝑁 → ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝑅 ) ) )
27 21 26 syl ( ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) ) → ( 𝑛𝑁 → ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝑅 ) ) )
28 27 imp ( ( ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) ) ∧ 𝑛𝑁 ) → ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑛 ) ) ∈ ( Base ‘ 𝑅 ) )
29 id ( 𝑛 = 𝑚𝑛 = 𝑚 )
30 fveq2 ( 𝑛 = 𝑚 → ( 𝑄𝑛 ) = ( 𝑄𝑚 ) )
31 29 30 oveq12d ( 𝑛 = 𝑚 → ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑛 ) ) = ( 𝑚 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑚 ) ) )
32 31 adantl ( ( ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) ) ∧ 𝑛 = 𝑚 ) → ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑛 ) ) = ( 𝑚 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑚 ) ) )
33 6 4 5 symgmatr01 ( ( 𝐾𝑁𝐿𝑁 ) → ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) → ∃ 𝑚𝑁 ( 𝑚 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑚 ) ) = 0 ) )
34 33 3adant1 ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) → ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) → ∃ 𝑚𝑁 ( 𝑚 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑚 ) ) = 0 ) )
35 34 imp ( ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) ) → ∃ 𝑚𝑁 ( 𝑚 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑚 ) ) = 0 )
36 7 4 8 12 28 32 35 gsummgp0 ( ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) ∧ 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) ) → ( 𝐺 Σg ( 𝑛𝑁 ↦ ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑛 ) ) ) ) = 0 )
37 36 ex ( ( 𝑀𝐵𝐾𝑁𝐿𝑁 ) → ( 𝑄 ∈ ( 𝑃 ∖ { 𝑞𝑃 ∣ ( 𝑞𝐾 ) = 𝐿 } ) → ( 𝐺 Σg ( 𝑛𝑁 ↦ ( 𝑛 ( 𝑖𝑁 , 𝑗𝑁 ↦ if ( 𝑖 = 𝐾 , if ( 𝑗 = 𝐿 , 1 , 0 ) , ( 𝑖 𝑀 𝑗 ) ) ) ( 𝑄𝑛 ) ) ) ) = 0 ) )