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 birani ⊢ M ∈ B ∧ K ∈ N → M ∈ Base A
24 23 adantr ⊢ M ∈ B ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → M ∈ Base A
25 eqid ⊢ Base R = Base R
26 1 25 matecl ⊢ i ∈ N ∧ j ∈ N ∧ M ∈ Base A → i M j ∈ Base R
27 20 21 24 26 syl3anc ⊢ M ∈ B ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → i M j ∈ Base R
28 7 25 mgpbas ⊢ Base R = Base G
29 27 28 eleqtrdi ⊢ M ∈ B ∧ K ∈ N ∧ i ∈ N ∧ j ∈ N → i M j ∈ Base G
30 29 ralrimivva ⊢ M ∈ B ∧ K ∈ N → ∀ i ∈ N ∀ j ∈ N i M j ∈ Base G
31 30 adantr ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ q ∈ P | q ⁡ K = K → ∀ i ∈ N ∀ j ∈ N i M j ∈ Base G
32 crngring ⊢ R ∈ CRing → R ∈ Ring
33 25 4 ring0cl ⊢ R ∈ Ring → 0 ˙ ∈ Base R
34 3 32 33 mp2b ⊢ 0 ˙ ∈ Base R
35 34 28 eleqtri ⊢ 0 ˙ ∈ Base G
36 31 35 jctir ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ q ∈ P | q ⁡ K = K → ∀ i ∈ N ∀ j ∈ N i M j ∈ Base G ∧ 0 ˙ ∈ Base G
37 simpr ⊢ M ∈ B ∧ K ∈ N → K ∈ N
38 37 adantr ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ q ∈ P | q ⁡ K = K → K ∈ N
39 simpr ⊢ M ∈ B ∧ K ∈ N ∧ p ∈ q ∈ P | q ⁡ K = K → p ∈ q ∈ P | q ⁡ K = K
40 eqid ⊢ q ∈ P | q ⁡ K = K = q ∈ P | q ⁡ K = K
41 7 5 ringidval ⊢ 1 ˙ = 0 G
42 eqid ⊢ Base G = Base G
43 6 40 41 42 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
44 19 36 38 38 39 43 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
45 44 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
46 45 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
47 46 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
48 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
49 47 48 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