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 ⊢ A = N Mat R
marep01ma.b ⊢ B = Base A
marep01ma.r ⊢ R ∈ CRing
marep01ma.0 ⊢ 0 ˙ = 0 R
marep01ma.1 ⊢ 1 ˙ = 1 R
smadiadetlem.p ⊢ P = Base SymGrp ⁡ N
smadiadetlem.g ⊢ G = mulGrp R
Assertion smadiadetlem0 ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → Q ∈ P ∖ q ∈ P | q ⁡ K = L → ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ n = 0 ˙

Proof

Step Hyp Ref Expression
1 marep01ma.a ⊢ A = N Mat R
2 marep01ma.b ⊢ B = Base A
3 marep01ma.r ⊢ R ∈ CRing
4 marep01ma.0 ⊢ 0 ˙ = 0 R
5 marep01ma.1 ⊢ 1 ˙ = 1 R
6 smadiadetlem.p ⊢ P = Base SymGrp ⁡ N
7 smadiadetlem.g ⊢ G = mulGrp R
8 3 a1i ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ Q ∈ P ∖ q ∈ P | q ⁡ K = L → R ∈ CRing
9 1 2 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
10 9 simpld ⊢ M ∈ B → N ∈ Fin
11 10 3ad2ant1 ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → N ∈ Fin
12 11 adantr ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ Q ∈ P ∖ q ∈ P | q ⁡ K = L → N ∈ Fin
13 crngring ⊢ R ∈ CRing → R ∈ Ring
14 3 13 mp1i ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ Q ∈ P ∖ q ∈ P | q ⁡ K = L → R ∈ Ring
15 eldifi ⊢ Q ∈ P ∖ q ∈ P | q ⁡ K = L → Q ∈ P
16 15 adantl ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ Q ∈ P ∖ q ∈ P | q ⁡ K = L → Q ∈ P
17 1 2 3 4 5 marep01ma ⊢ M ∈ B → i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j ∈ B
18 17 3ad2ant1 ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j ∈ B
19 18 adantr ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ Q ∈ P ∖ q ∈ P | q ⁡ K = L → i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j ∈ B
20 1 2 6 matepm2cl ⊢ R ∈ Ring ∧ Q ∈ P ∧ i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j ∈ B → ∀ m ∈ N m i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ m ∈ Base R
21 14 16 19 20 syl3anc ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ Q ∈ P ∖ q ∈ P | q ⁡ K = L → ∀ m ∈ N m i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ m ∈ Base R
22 id ⊢ m = n → m = n
23 fveq2 ⊢ m = n → Q ⁡ m = Q ⁡ n
24 22 23 oveq12d ⊢ m = n → m i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ m = n i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ n
25 24 eleq1d ⊢ m = n → m i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ m ∈ Base R ↔ n i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ n ∈ Base R
26 25 rspccv ⊢ ∀ m ∈ N m i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ m ∈ Base R → n ∈ N → n i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ n ∈ Base R
27 21 26 syl ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ Q ∈ P ∖ q ∈ P | q ⁡ K = L → n ∈ N → n i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ n ∈ Base R
28 27 imp ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ Q ∈ P ∖ q ∈ P | q ⁡ K = L ∧ n ∈ N → n i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ n ∈ Base R
29 id ⊢ n = m → n = m
30 fveq2 ⊢ n = m → Q ⁡ n = Q ⁡ m
31 29 30 oveq12d ⊢ n = m → n i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ n = m i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ m
32 31 adantl ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ Q ∈ P ∖ q ∈ P | q ⁡ K = L ∧ n = m → n i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ n = m i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ m
33 6 4 5 symgmatr01 ⊢ K ∈ N ∧ L ∈ N → Q ∈ P ∖ q ∈ P | q ⁡ K = L → ∃ m ∈ N m i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ m = 0 ˙
34 33 3adant1 ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → Q ∈ P ∖ q ∈ P | q ⁡ K = L → ∃ m ∈ N m i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ m = 0 ˙
35 34 imp ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ Q ∈ P ∖ q ∈ P | q ⁡ K = L → ∃ m ∈ N m i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ m = 0 ˙
36 7 4 8 12 28 32 35 gsummgp0 ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N ∧ Q ∈ P ∖ q ∈ P | q ⁡ K = L → ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ n = 0 ˙
37 36 ex ⊢ M ∈ B ∧ K ∈ N ∧ L ∈ N → Q ∈ P ∖ q ∈ P | q ⁡ K = L → ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = L 1 ˙ 0 ˙ i M j Q ⁡ n = 0 ˙