smadiadetlem3lem0

	Ref	Expression
Hypotheses	marep01ma.a	$⊢ A = N Mat R$
	marep01ma.b	$⊢ B = {Base}_{A}$
	marep01ma.r	$⊢ R \in CRing$
	marep01ma.0	$⊢ \underset{˙}{0} = 0_{R}$
	marep01ma.1	$⊢ \underset{˙}{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	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
	smadiadetlem.w	$⊢ W = {Base}_{SymGrp (N ∖ \{K\})}$
	smadiadetlem.z	$⊢ Z = pmSgn (N ∖ \{K\})$
Assertion	smadiadetlem3lem0	$⊢ ((M \in B \land K \in N) \land Q \in W) \to (Y \circ Z) (Q) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) Q (n))) \in {Base}_{R}$

Proof

Step	Hyp	Ref	Expression
1		marep01ma.a	$⊢ A = N Mat R$
2		marep01ma.b	$⊢ B = {Base}_{A}$
3		marep01ma.r	$⊢ R \in CRing$
4		marep01ma.0	$⊢ \underset{˙}{0} = 0_{R}$
5		marep01ma.1	$⊢ \underset{˙}{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	$⊢ \underset{˙}{\cdot} = \cdot_{R}$
11		smadiadetlem.w	$⊢ W = {Base}_{SymGrp (N ∖ \{K\})}$
12		smadiadetlem.z	$⊢ Z = pmSgn (N ∖ \{K\})$
13		difssd	$⊢ K \in N \to N ∖ \{K\} \subseteq N$
14	13	anim2i	$⊢ (M \in B \land K \in N) \to (M \in B \land N ∖ \{K\} \subseteq N)$
15	14	adantr	$⊢ ((M \in B \land K \in N) \land Q \in W) \to (M \in B \land N ∖ \{K\} \subseteq N)$
16	1 2	submabas	$⊢ (M \in B \land N ∖ \{K\} \subseteq N) \to (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) \in {Base}_{((N ∖ \{K\}) Mat R)}$
17	15 16	syl	$⊢ ((M \in B \land K \in N) \land Q \in W) \to (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) \in {Base}_{((N ∖ \{K\}) Mat R)}$
18		simpr	$⊢ ((M \in B \land K \in N) \land Q \in W) \to Q \in 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 \in CRing \land (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) \in {Base}_{((N ∖ \{K\}) Mat R)} \land Q \in W) \to (Y \circ Z) (Q) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) Q (n))) \in {Base}_{R}$
22	3 17 18 21	mp3an2i	$⊢ ((M \in B \land K \in N) \land Q \in W) \to (Y \circ Z) (Q) \cdot_{R} (\underset{n \in N ∖ \{K\}}{\sum_{G}}, (n (i \in (N ∖ \{K\}), j \in (N ∖ \{K\}) ⟼ i M j) Q (n))) \in {Base}_{R}$

Metamath Proof Explorer

Theorem smadiadetlem3lem0

Proof