Theorem smadiadetlem3lem1

Description: Lemma 1 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 e. CRing
	marep01ma.0	|- .0. = ( 0g ` R )
	marep01ma.1	|- .1. = ( 1r ` R )
	smadiadetlem.p	|- P = ( Base ` ( SymGrp ` N ) )
	smadiadetlem.g	|- G = ( mulGrp ` R )
	madetminlem.y	|- Y = ( ZRHom ` R )
	madetminlem.s	|- S = ( pmSgn ` N )
	madetminlem.t	|- .x. = ( .r ` R )
	smadiadetlem.w	|- W = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
	smadiadetlem.z	|- Z = ( pmSgn ` ( N \ { K } ) )
Assertion	smadiadetlem3lem1	|- ( ( M e. B /\ K e. N ) -> ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) : W --> ( Base ` R ) )

Proof

Step	Hyp	Ref	Expression
1		marep01ma.a	|- A = ( N Mat R )
2		marep01ma.b	|- B = ( Base ` A )
3		marep01ma.r	|- R e. CRing
4		marep01ma.0	|- .0. = ( 0g ` R )
5		marep01ma.1	|- .1. = ( 1r ` R )
6		smadiadetlem.p	|- P = ( Base ` ( SymGrp ` N ) )
7		smadiadetlem.g	|- G = ( mulGrp ` R )
8		madetminlem.y	|- Y = ( ZRHom ` R )
9		madetminlem.s	|- S = ( pmSgn ` N )
10		madetminlem.t	|- .x. = ( .r ` R )
11		smadiadetlem.w	|- W = ( Base ` ( SymGrp ` ( N \ { K } ) ) )
12		smadiadetlem.z	|- Z = ( pmSgn ` ( N \ { K } ) )
13	1 2 3 4 5 6 7 8 9 10 11 12	smadiadetlem3lem0	|- ( ( ( M e. B /\ K e. N ) /\ p e. W ) -> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) e. ( Base ` R ) )
14	13	fmpttd	|- ( ( M e. B /\ K e. N ) -> ( p e. W |-> ( ( ( Y o. Z ) ` p ) ( .r ` R ) ( G gsum ( n e. ( N \ { K } ) |-> ( n ( i e. ( N \ { K } ) , j e. ( N \ { K } ) |-> ( i M j ) ) ( p ` n ) ) ) ) ) ) : W --> ( Base ` R ) )