Metamath Proof Explorer

Theorem smadiadetlem3lem0

Description: Lemma 0 for smadiadetlem3 . (Contributed by AV, 12-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 smadiadetlem3lem0 ⊢ M ∈ B ∧ K ∈ N ∧ Q ∈ W → Y ∘ Z ⁡ Q ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j Q ⁡ n ∈ Base R

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 difssd ⊢ K ∈ N → N ∖ K ⊆ N
14 13 anim2i ⊢ M ∈ B ∧ K ∈ N → M ∈ B ∧ N ∖ K ⊆ N
15 14 adantr ⊢ M ∈ B ∧ K ∈ N ∧ Q ∈ W → M ∈ B ∧ N ∖ K ⊆ N
16 1 2 submabas ⊢ M ∈ B ∧ N ∖ K ⊆ N → i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j ∈ Base N ∖ K Mat R
17 15 16 syl ⊢ M ∈ B ∧ K ∈ N ∧ Q ∈ W → i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j ∈ Base N ∖ K Mat R
18 simpr ⊢ M ∈ B ∧ K ∈ N ∧ Q ∈ W → Q ∈ W
19 eqid ⊢ N ∖ K Mat R = N ∖ K Mat R
20 eqid ⊢ Base N ∖ K Mat R = Base N ∖ K Mat R
21 11 12 8 19 20 7 madetsmelbas2 ⊢ R ∈ CRing ∧ i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j ∈ Base N ∖ K Mat R ∧ Q ∈ W → Y ∘ Z ⁡ Q ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j Q ⁡ n ∈ Base R
22 3 17 18 21 mp3an2i ⊢ M ∈ B ∧ K ∈ N ∧ Q ∈ W → Y ∘ Z ⁡ Q ⋅ R ∑ G n ∈ N ∖ K n i ∈ N ∖ K , j ∈ N ∖ K ⟼ i M j Q ⁡ n ∈ Base R