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