Theorem 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 e. Ring /\ Q e. P /\ M e. B ) -> ( G gsum ( n e. N |-> ( ( Q ` n ) M n ) ) ) e. ( Base ` R ) )

Proof

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 e. Ring -> G e. Mnd )
9	8	3ad2ant1	|- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> G e. Mnd )
10		2eluzge1	|- 2 e. ( ZZ>= ` 1 )
11	10	a1i	|- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> 2 e. ( ZZ>= ` 1 ) )
12		1z	|- 1 e. ZZ
13		fzpr	|- ( 1 e. ZZ -> ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) } )
14	12 13	ax-mp	|- ( 1 ... ( 1 + 1 ) ) = { 1 , ( 1 + 1 ) }
15		1p1e2	|- ( 1 + 1 ) = 2
16	15	preq2i	|- { 1 , ( 1 + 1 ) } = { 1 , 2 }
17	14 16	eqtri	|- ( 1 ... ( 1 + 1 ) ) = { 1 , 2 }
18		df-2	|- 2 = ( 1 + 1 )
19	18	oveq2i	|- ( 1 ... 2 ) = ( 1 ... ( 1 + 1 ) )
20	17 19 1	3eqtr4ri	|- N = ( 1 ... 2 )
21	20	a1i	|- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> N = ( 1 ... 2 ) )
22	3 4 2	matepmcl	|- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> A. n e. N ( ( Q ` n ) M n ) e. ( Base ` R ) )
23	7 9 11 21 22	gsummptfzcl	|- ( ( R e. Ring /\ Q e. P /\ M e. B ) -> ( G gsum ( n e. N |-> ( ( Q ` n ) M n ) ) ) e. ( Base ` R ) )