m2detleiblem2

Description: Lemma 2 for m2detleib . (Contributed by AV, 16-Dec-2018) (Proof shortened by AV, 1-Jan-2019)

	Ref	Expression
Hypotheses	m2detleiblem2.n	$⊢ N = \{1, 2\}$
	m2detleiblem2.p	$⊢ P = {Base}_{SymGrp (N)}$
	m2detleiblem2.a	$⊢ A = N Mat R$
	m2detleiblem2.b	$⊢ B = {Base}_{A}$
	m2detleiblem2.g	$⊢ G = {mulGrp}_{R}$
Assertion	m2detleiblem2	$⊢ (R \in Ring \land Q \in P \land M \in B) \to \underset{n \in N}{\sum_{G}} (Q (n) M n) \in {Base}_{R}$

Step	Hyp	Ref	Expression
1		m2detleiblem2.n	$⊢ N = \{1, 2\}$
2		m2detleiblem2.p	$⊢ P = {Base}_{SymGrp (N)}$
3		m2detleiblem2.a	$⊢ A = N Mat R$
4		m2detleiblem2.b	$⊢ B = {Base}_{A}$
5		m2detleiblem2.g	$⊢ G = {mulGrp}_{R}$
6		eqid	$⊢ {Base}_{R} = {Base}_{R}$
7	5 6	mgpbas	$⊢ {Base}_{R} = {Base}_{G}$
8	5	ringmgp	$⊢ R \in Ring \to G \in Mnd$
9	8	3ad2ant1	$⊢ (R \in Ring \land Q \in P \land M \in B) \to G \in Mnd$
10		2eluzge1	$⊢ 2 \in ℤ_{\geq 1}$
11	10	a1i	$⊢ (R \in Ring \land Q \in P \land M \in B) \to 2 \in ℤ_{\geq 1}$
12		1z	$⊢ 1 \in ℤ$
13		fzpr	$⊢ 1 \in ℤ \to (1 \dots 1 + 1) = \{1, 1 + 1\}$
14	12 13	ax-mp	$⊢ (1 \dots 1 + 1) = \{1, 1 + 1\}$
15		1p1e2	$⊢ 1 + 1 = 2$
16	15	preq2i	$⊢ \{1, 1 + 1\} = \{1, 2\}$
17	14 16	eqtri	$⊢ (1 \dots 1 + 1) = \{1, 2\}$
18		df-2	$⊢ 2 = 1 + 1$
19	18	oveq2i	$⊢ (1 \dots 2) = (1 \dots 1 + 1)$
20	17 19 1	3eqtr4ri	$⊢ N = (1 \dots 2)$
21	20	a1i	$⊢ (R \in Ring \land Q \in P \land M \in B) \to N = (1 \dots 2)$
22	3 4 2	matepmcl	$⊢ (R \in Ring \land Q \in P \land M \in B) \to \forall n \in N Q (n) M n \in {Base}_{R}$
23	7 9 11 21 22	gsummptfzcl	$⊢ (R \in Ring \land Q \in P \land M \in B) \to \underset{n \in N}{\sum_{G}} (Q (n) M n) \in {Base}_{R}$

Metamath Proof Explorer