Metamath Proof Explorer

Theorem smadiadetlem4

Description: Lemma 4 for smadiadet . (Contributed by AV, 31-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
madetminlem.y ⊢ Y = ℤRHom ⁡ R
madetminlem.s ⊢ S = pmSgn ⁡ N
madetminlem.t ⊢ · ˙ = ⋅ R
smadiadetlem.w ⊢ W = Base SymGrp ⁡ N ∖ K
smadiadetlem.z ⊢ Z = pmSgn ⁡ N ∖ K
Assertion smadiadetlem4 ⊢ M ∈ B ∧ K ∈ N → ∑ R p ∈ q ∈ P | q ⁡ K = K Y ∘ S ⁡ p ⋅ R ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j p ⁡ n = ∑ R p ∈ W Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n

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 madetminlem.y ⊢ Y = ℤRHom ⁡ R
9 madetminlem.s ⊢ S = pmSgn ⁡ N
10 madetminlem.t ⊢ · ˙ = ⋅ R
11 smadiadetlem.w ⊢ W = Base SymGrp ⁡ N ∖ K
12 smadiadetlem.z ⊢ Z = pmSgn ⁡ N ∖ K
13 7 crngmgp ⊢ R ∈ CRing → G ∈ CMnd
14 3 13 mp1i ⊢ M ∈ B ∧ K ∈ N → G ∈ CMnd
15 1 2 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
16 15 simpld ⊢ M ∈ B → N ∈ Fin
17 16 adantr ⊢ M ∈ B ∧ K ∈ N → N ∈ Fin
18 14 17 jca ⊢ M ∈ B ∧ K ∈ N → G ∈ CMnd ∧ N ∈ Fin
19 18 adantr ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ q ∈ P | q ⁡ K = K → G ∈ CMnd ∧ N ∈ Fin
20 simprl ⊢ M ∈ B ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → i ∈ N
21 simprr ⊢ M ∈ B ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → j ∈ N
22 2 eleq2i ⊢ M ∈ B ↔ M ∈ Base A
23 22 biimpi ⊢ M ∈ B → M ∈ Base A
24 23 adantr ⊢ M ∈ B ∧ K ∈ N → M ∈ Base A
25 24 adantr ⊢ M ∈ B ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → M ∈ Base A
26 eqid ⊢ Base R = Base R
27 1 26 matecl ⊢ i ∈ N ∧ j ∈ N ∧ M ∈ Base A → i M j ∈ Base R
28 20 21 25 27 syl3anc ⊢ M ∈ B ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → i M j ∈ Base R
29 7 26 mgpbas ⊢ Base R = Base G
30 28 29 eleqtrdi ⊢ M ∈ B ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → i M j ∈ Base G
31 30 ralrimivva ⊢ M ∈ B ∧ K ∈ N → ∀ i ∈ N ∀ j ∈ N i M j ∈ Base G
32 31 adantr ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ q ∈ P | q ⁡ K = K → ∀ i ∈ N ∀ j ∈ N i M j ∈ Base G
33 crngring ⊢ R ∈ CRing → R ∈ Ring
34 26 4 ring0cl ⊢ R ∈ Ring → 0 ˙ ∈ Base R
35 3 33 34 mp2b ⊢ 0 ˙ ∈ Base R
36 35 29 eleqtri ⊢ 0 ˙ ∈ Base G
37 32 36 jctir ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ q ∈ P | q ⁡ K = K → ∀ i ∈ N ∀ j ∈ N i M j ∈ Base G ∧ 0 ˙ ∈ Base G
38 simpr ⊢ M ∈ B ∧ K ∈ N → K ∈ N
39 38 adantr ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ q ∈ P | q ⁡ K = K → K ∈ N
40 simpr ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ q ∈ P | q ⁡ K = K → p ∈ q ∈ P | q ⁡ K = K
41 eqid ⊢ q ∈ P | q ⁡ K = K = q ∈ P | q ⁡ K = K
42 7 5 ringidval ⊢ 1 ˙ = 0 G
43 eqid ⊢ Base G = Base G
44 6 41 42 43 gsummatr01 ⊢ G ∈ CMnd ∧ N ∈ Fin ∧ ∀ i ∈ N ∀ j ∈ N i M j ∈ Base G ∧ 0 ˙ ∈ Base G ∧ K ∈ N ∧ K ∈ N ∧ p ∈ q ∈ P | q ⁡ K = K → ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j p ⁡ n = ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
45 19 37 39 39 40 44 syl113anc ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ q ∈ P | q ⁡ K = K → ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j p ⁡ n = ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
46 45 oveq2d ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ q ∈ P | q ⁡ K = K → Y ∘ S ⁡ p ⋅ R ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j p ⁡ n = Y ∘ S ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
47 46 mpteq2dva ⊢ M ∈ B ∧ K ∈ N → p ∈ q ∈ P | q ⁡ K = K ⟼ Y ∘ S ⁡ p ⋅ R ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j p ⁡ n = p ∈ q ∈ P | q ⁡ K = K ⟼ Y ∘ S ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
48 47 oveq2d ⊢ M ∈ B ∧ K ∈ N → ∑ R p ∈ q ∈ P | q ⁡ K = K Y ∘ S ⁡ p ⋅ R ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j p ⁡ n = ∑ R p ∈ q ∈ P | q ⁡ K = K Y ∘ S ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
49 1 2 3 4 5 6 7 8 9 10 11 12 smadiadetlem3 ⊢ M ∈ B ∧ K ∈ N → ∑ R p ∈ q ∈ P | q ⁡ K = K Y ∘ S ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n = ∑ R p ∈ W Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n
50 48 49 eqtrd ⊢ M ∈ B ∧ K ∈ N → ∑ R p ∈ q ∈ P | q ⁡ K = K Y ∘ S ⁡ p ⋅ R ∑ G n ∈ N n i ∈ N , j ∈ N ⟼ if i = K if j = K 1 ˙ 0 ˙ i M j p ⁡ n = ∑ R p ∈ W Y ∘ Z ⁡ p ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j p ⁡ n