P. 299 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 29801-29900   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	orngogrp 29801	An ordered ring is an ordered group. (Contributed by Thierry Arnoux, 23-Mar-2018.)
|- ( R e. oRing -> R e. oGrp )
Theorem	isofld 29802	An ordered field is a field with a total ordering compatible with its operations. (Contributed by Thierry Arnoux, 23-Mar-2018.)
|- ( F e. oField <-> ( F e. Field /\ F e. oRing ) )
Theorem	orngmul 29803	In an ordered ring, the ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 20-Jan-2018.)
|- B = ( Base ` R )   &    |- .<_ = ( le ` R )   &    |- .0. = ( 0g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. oRing /\ ( X e. B /\ .0. .<_ X ) /\ ( Y e. B /\ .0. .<_ Y ) ) -> .0. .<_ ( X .x. Y ) )
Theorem	orngsqr 29804	In an ordered ring, all squares are positive. (Contributed by Thierry Arnoux, 20-Jan-2018.)
|- B = ( Base ` R )   &    |- .<_ = ( le ` R )   &    |- .0. = ( 0g ` R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. oRing /\ X e. B ) -> .0. .<_ ( X .x. X ) )
Theorem	ornglmulle 29805	In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> R e. oRing )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- .<_ = ( le ` R )   &    |- ( ph -> X .<_ Y )   &    |- ( ph -> .0. .<_ Z )   =>    |- ( ph -> ( Z .x. X ) .<_ ( Z .x. Y ) )
Theorem	orngrmulle 29806	In an ordered ring, multiplication with a positive does not change comparison. (Contributed by Thierry Arnoux, 10-Apr-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> R e. oRing )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- .<_ = ( le ` R )   &    |- ( ph -> X .<_ Y )   &    |- ( ph -> .0. .<_ Z )   =>    |- ( ph -> ( X .x. Z ) .<_ ( Y .x. Z ) )
Theorem	ornglmullt 29807	In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> R e. oRing )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- .< = ( lt ` R )   &    |- ( ph -> R e. DivRing )   &    |- ( ph -> X .< Y )   &    |- ( ph -> .0. .< Z )   =>    |- ( ph -> ( Z .x. X ) .< ( Z .x. Y ) )
Theorem	orngrmullt 29808	In an ordered ring, multiplication with a positive does not change strict comparison. (Contributed by Thierry Arnoux, 9-Apr-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- ( ph -> R e. oRing )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> Z e. B )   &    |- .< = ( lt ` R )   &    |- ( ph -> R e. DivRing )   &    |- ( ph -> X .< Y )   &    |- ( ph -> .0. .< Z )   =>    |- ( ph -> ( X .x. Z ) .< ( Y .x. Z ) )
Theorem	orngmullt 29809	In an ordered ring, the strict ordering is compatible with the ring multiplication operation. (Contributed by Thierry Arnoux, 9-Sep-2018.)
|- B = ( Base ` R )   &    |- .x. = ( .r ` R )   &    |- .0. = ( 0g ` R )   &    |- .< = ( lt ` R )   &    |- ( ph -> R e. oRing )   &    |- ( ph -> R e. DivRing )   &    |- ( ph -> X e. B )   &    |- ( ph -> Y e. B )   &    |- ( ph -> .0. .< X )   &    |- ( ph -> .0. .< Y )   =>    |- ( ph -> .0. .< ( X .x. Y ) )
Theorem	ofldfld 29810	An ordered field is a field. (Contributed by Thierry Arnoux, 20-Jan-2018.)
|- ( F e. oField -> F e. Field )
Theorem	ofldtos 29811	An ordered field is a totally ordered set. (Contributed by Thierry Arnoux, 20-Jan-2018.)
|- ( F e. oField -> F e. Toset )
Theorem	orng0le1 29812	In an ordered ring, the ring unit is positive. (Contributed by Thierry Arnoux, 21-Jan-2018.)
|- .0. = ( 0g ` F )   &    |- .1. = ( 1r ` F )   &    |- .<_ = ( le ` F )   =>    |- ( F e. oRing -> .0. .<_ .1. )
Theorem	ofldlt1 29813	In an ordered field, the ring unit is strictly positive. (Contributed by Thierry Arnoux, 21-Jan-2018.)
|- .0. = ( 0g ` F )   &    |- .1. = ( 1r ` F )   &    |- .< = ( lt ` F )   =>    |- ( F e. oField -> .0. .< .1. )
Theorem	ofldchr 29814	The characteristic of an ordered field is zero. (Contributed by Thierry Arnoux, 21-Jan-2018.) (Proof shortened by AV, 6-Oct-2020.)
|- ( F e. oField -> (chr ` F ) = 0 )
Theorem	suborng 29815	Every subring of an ordered ring is also an ordered ring. (Contributed by Thierry Arnoux, 21-Jan-2018.)
|- ( ( R e. oRing /\ ( R ↾s A ) e. Ring ) -> ( R ↾s A ) e. oRing )
Theorem	subofld 29816	Every subfield of an ordered field is also an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.)
|- ( ( F e. oField /\ ( F ↾s A ) e. Field ) -> ( F ↾s A ) e. oField )
Theorem	isarchiofld 29817*	Axiom of Archimedes : a characterization of the Archimedean property for ordered fields. (Contributed by Thierry Arnoux, 9-Apr-2018.)
|- B = ( Base ` W )   &    |- H = ( ZRHom ` W )   &    |- .< = ( lt ` W )   =>    |- ( W e. oField -> ( W e. Archi <-> A. x e. B E. n e. NN x .< ( H ` n ) ) )
20.3.9.9  Ring homomorphisms - misc additions
Theorem	rhmdvdsr 29818	A ring homomorphism preserves the divisibility relation. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- X = ( Base ` R )   &    |- .|| = ( ||r ` R )   &    |- ./ = ( ||r ` S )   =>    |- ( ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) /\ A .|| B ) -> ( F ` A ) ./ ( F ` B ) )
Theorem	rhmopp 29819	A ring homomorphism is also a ring homomorphism for the opposite rings. (Contributed by Thierry Arnoux, 27-Oct-2017.)
|- ( F e. ( R RingHom S ) -> F e. ( (oppr ` R ) RingHom (oppr ` S ) ) )
Theorem	elrhmunit 29820	Ring homomorphisms preserve unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.)
|- ( ( F e. ( R RingHom S ) /\ A e. (Unit ` R ) ) -> ( F ` A ) e. (Unit ` S ) )
Theorem	rhmdvd 29821	A ring homomorphism preserves ratios. (Contributed by Thierry Arnoux, 22-Oct-2017.)
|- U = (Unit ` S )   &    |- X = ( Base ` R )   &    |- ./ = (/r ` S )   &    |- .x. = ( .r ` R )   =>    |- ( ( F e. ( R RingHom S ) /\ ( A e. X /\ B e. X /\ C e. X ) /\ ( ( F ` B ) e. U /\ ( F ` C ) e. U ) ) -> ( ( F ` A ) ./ ( F ` B ) ) = ( ( F ` ( A .x. C ) ) ./ ( F ` ( B .x. C ) ) ) )
Theorem	rhmunitinv 29822	Ring homomorphisms preserve the inverse of unit elements. (Contributed by Thierry Arnoux, 23-Oct-2017.)
|- ( ( F e. ( R RingHom S ) /\ A e. (Unit ` R ) ) -> ( F ` ( ( invr ` R ) ` A ) ) = ( ( invr ` S ) ` ( F ` A ) ) )
Theorem	kerunit 29823	If a unit element lies in the kernel of a ring homomorphism, then 0 = 1, i.e. the target ring is the zero ring. (Contributed by Thierry Arnoux, 24-Oct-2017.)
|- U = (Unit ` R )   &    |- .0. = ( 0g ` S )   &    |- .1. = ( 1r ` S )   =>    |- ( ( F e. ( R RingHom S ) /\ ( U i^i ( `' F " { .0. } ) ) =/= (/) ) -> .1. = .0. )
20.3.9.10  Scalar restriction operation
Syntax	cresv 29824	Extend class notation with the scalar restriction operation.
class ↾v
Definition	df-resv 29825*	Define an operator to restrict the scalar field component of an extended structure. (Contributed by Thierry Arnoux, 5-Sep-2018.)
|- ↾v = ( w e. _V , x e. _V |-> if ( ( Base ` (Scalar ` w ) ) C_ x , w , ( w sSet <. (Scalar ` ndx ) , ( (Scalar ` w ) ↾s x ) >. ) ) )
Theorem	reldmresv 29826	The scalar restriction is a proper operator, so it can be used with ovprc1 6684. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- Rel dom ↾v
Theorem	resvval 29827	Value of structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- R = ( W ↾v A )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   =>    |- ( ( W e. X /\ A e. Y ) -> R = if ( B C_ A , W , ( W sSet <. (Scalar ` ndx ) , ( F ↾s A ) >. ) ) )
Theorem	resvid2 29828	General behavior of trivial restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- R = ( W ↾v A )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   =>    |- ( ( B C_ A /\ W e. X /\ A e. Y ) -> R = W )
Theorem	resvval2 29829	Value of nontrivial structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- R = ( W ↾v A )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   =>    |- ( ( -. B C_ A /\ W e. X /\ A e. Y ) -> R = ( W sSet <. (Scalar ` ndx ) , ( F ↾s A ) >. ) )
Theorem	resvsca 29830	Base set of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- R = ( W ↾v A )   &    |- F = (Scalar ` W )   &    |- B = ( Base ` F )   =>    |- ( A e. V -> ( F ↾s A ) = (Scalar ` R ) )
Theorem	resvlem 29831	Other elements of a structure restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- R = ( W ↾v A )   &    |- C = ( E ` W )   &    |- E = Slot N   &    |- N e. NN   &    |- N =/= 5   =>    |- ( A e. V -> C = ( E ` R ) )
Theorem	resvbas 29832	Base is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- H = ( G ↾v A )   &    |- B = ( Base ` G )   =>    |- ( A e. V -> B = ( Base ` H ) )
Theorem	resvplusg 29833	+g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- H = ( G ↾v A )   &    |- .+ = ( +g ` G )   =>    |- ( A e. V -> .+ = ( +g ` H ) )
Theorem	resvvsca 29834	.s is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- H = ( G ↾v A )   &    |- .x. = ( .s ` G )   =>    |- ( A e. V -> .x. = ( .s ` H ) )
Theorem	resvmulr 29835	.s is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- H = ( G ↾v A )   &    |- .x. = ( .r ` G )   =>    |- ( A e. V -> .x. = ( .r ` H ) )
Theorem	resv0g 29836	0g is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- H = ( G ↾v A )   &    |- .0. = ( 0g ` G )   =>    |- ( A e. V -> .0. = ( 0g ` H ) )
Theorem	resv1r 29837	1r is unaffected by scalar restriction. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- H = ( G ↾v A )   &    |- .1. = ( 1r ` G )   =>    |- ( A e. V -> .1. = ( 1r ` H ) )
Theorem	resvcmn 29838	Scalar restriction preserves commutative monoids. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- H = ( G ↾v A )   =>    |- ( A e. V -> ( G e. CMnd <-> H e. CMnd ) )
20.3.9.11  The commutative ring of gaussian integers
Theorem	gzcrng 29839	The gaussian integers form a commutative ring. (Contributed by Thierry Arnoux, 18-Mar-2018.)
|- (ℂfld ↾s ZZ[_i] ) e. CRing
20.3.9.12  The archimedean ordered field of real numbers
Theorem	reofld 29840	The real numbers form an ordered field. (Contributed by Thierry Arnoux, 21-Jan-2018.)
|- RRfld e. oField
Theorem	nn0omnd 29841	The nonnegative integers form an ordered monoid. (Contributed by Thierry Arnoux, 23-Mar-2018.)
|- (ℂfld ↾s NN0 ) e. oMnd
Theorem	rearchi 29842	The field of the real numbers is Archimedean. See also arch 11289. (Contributed by Thierry Arnoux, 9-Apr-2018.)
|- RRfld e. Archi
Theorem	nn0archi 29843	The monoid of the nonnegative integers is Archimedean. (Contributed by Thierry Arnoux, 16-Sep-2018.)
|- (ℂfld ↾s NN0 ) e. Archi
Theorem	xrge0slmod 29844	The extended nonnegative real numbers form a semiring left module. One could also have used subringAlg to get the same structure. (Contributed by Thierry Arnoux, 6-Sep-2018.)
|- G = ( RR*s ↾s ( 0 [,] +oo ) )   &    |- W = ( G ↾v ( 0 [,) +oo ) )   =>    |- W e. SLMod
20.3.10  Matrices
20.3.10.1  The symmetric group
Theorem	symgfcoeu 29845*	Uniqueness property of permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.)
|- G = ( Base ` ( SymGrp ` D ) )   =>    |- ( ( D e. V /\ P e. G /\ Q e. G ) -> E! p e. G Q = ( P o. p ) )
20.3.10.2  Permutation Signs
Theorem	psgndmfi 29846	For a finite base set, the permutation sign is defined for all permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.)
|- S = (pmSgn ` D )   &    |- G = ( Base ` ( SymGrp ` D ) )   =>    |- ( D e. Fin -> S Fn G )
Theorem	psgnid 29847	Permutation sign of the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.)
|- S = (pmSgn ` D )   =>    |- ( D e. Fin -> ( S ` ( _I |` D ) ) = 1 )
Theorem	pmtrprfv2 29848	In a transposition of two given points, each maps to the other. (Contributed by Thierry Arnoux, 22-Aug-2020.)
|- T = (pmTrsp ` D )   =>    |- ( ( D e. V /\ ( X e. D /\ Y e. D /\ X =/= Y ) ) -> ( ( T ` { X , Y } ) ` Y ) = X )
Theorem	pmtrto1cl 29849	Useful lemma for the following theorems. (Contributed by Thierry Arnoux, 21-Aug-2020.)
|- D = ( 1 ... N )   &    |- T = (pmTrsp ` D )   =>    |- ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( T ` { K , ( K + 1 ) } ) e. ran T )
Theorem	psgnfzto1stlem 29850*	Lemma for psgnfzto1st 29855. Our permutation of rank ( n + 1 ) can be written as a permutation of rank n composed with a transposition. (Contributed by Thierry Arnoux, 21-Aug-2020.)
|- D = ( 1 ... N )   =>    |- ( ( K e. NN /\ ( K + 1 ) e. D ) -> ( i e. D |-> if ( i = 1 , ( K + 1 ) , if ( i <_ ( K + 1 ) , ( i - 1 ) , i ) ) ) = ( ( (pmTrsp ` D ) ` { K , ( K + 1 ) } ) o. ( i e. D |-> if ( i = 1 , K , if ( i <_ K , ( i - 1 ) , i ) ) ) ) )
Theorem	fzto1stfv1 29851*	Value of our permutation P at 1. (Contributed by Thierry Arnoux, 23-Aug-2020.)
|- D = ( 1 ... N )   &    |- P = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )   =>    |- ( I e. D -> ( P ` 1 ) = I )
Theorem	fzto1st1 29852*	Special case where the permutation defined in psgnfzto1st 29855 is the identity. (Contributed by Thierry Arnoux, 21-Aug-2020.)
|- D = ( 1 ... N )   &    |- P = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )   =>    |- ( I = 1 -> P = ( _I |` D ) )
Theorem	fzto1st 29853*	The function moving one element to the first position (and shifting all elements before it) is a permutation. (Contributed by Thierry Arnoux, 21-Aug-2020.)
|- D = ( 1 ... N )   &    |- P = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )   &    |- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   =>    |- ( I e. D -> P e. B )
Theorem	fzto1stinvn 29854*	Value of the inverse of our permutation P at I (Contributed by Thierry Arnoux, 23-Aug-2020.)
|- D = ( 1 ... N )   &    |- P = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )   &    |- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   =>    |- ( I e. D -> ( `' P ` I ) = 1 )
Theorem	psgnfzto1st 29855*	The permutation sign for moving one element to the first position. (Contributed by Thierry Arnoux, 21-Aug-2020.)
|- D = ( 1 ... N )   &    |- P = ( i e. D |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )   &    |- G = ( SymGrp ` D )   &    |- B = ( Base ` G )   &    |- S = (pmSgn ` D )   =>    |- ( I e. D -> ( S ` P ) = ( -u 1 ^ ( I + 1 ) ) )
20.3.10.3  Transpositions
Theorem	pmtridf1o 29856	Transpositions of X and Y (understood to be the identity when X = Y), are bijections. (Contributed by Thierry Arnoux, 1-Jan-2022.)
|- ( ph -> A e. V )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- T = if ( X = Y , ( _I |` A ) , ( (pmTrsp ` A ) ` { X , Y } ) )   =>    |- ( ph -> T : A -1-1-onto-> A )
Theorem	pmtridfv1 29857	Value at X of the transposition of X and Y (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022.)
|- ( ph -> A e. V )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- T = if ( X = Y , ( _I |` A ) , ( (pmTrsp ` A ) ` { X , Y } ) )   =>    |- ( ph -> ( T ` X ) = Y )
Theorem	pmtridfv2 29858	Value at Y of the transposition of X and Y (understood to be the identity when X = Y ). (Contributed by Thierry Arnoux, 3-Jan-2022.)
|- ( ph -> A e. V )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. A )   &    |- T = if ( X = Y , ( _I |` A ) , ( (pmTrsp ` A ) ` { X , Y } ) )   =>    |- ( ph -> ( T ` Y ) = X )
20.3.10.4  Submatrices
Syntax	csmat 29859	Syntax for a function generating submatrixes.
class subMat1
Definition	df-smat 29860*	Define a function generating submatrices of an integer-indexed matrix. The function maps an index in ( ( 1 ... M ) X. ( 1 ... N ) ) into a new index in ( ( 1 ... ( M - 1 ) ) X. ( 1 ... ( N - 1 ) ) ). A submatrix is obtained by deleting a row and a column of the original matrix. Because this function re-indexes the matrix, the resulting submatrix still has the same index set for rows and columns, and its determinent is defined, unlike the current df-subma 20383. (Contributed by Thierry Arnoux, 18-Aug-2020.)
|- subMat1 = ( m e. _V |-> ( k e. NN , l e. NN |-> ( m o. ( i e. NN , j e. NN |-> <. if ( i < k , i , ( i + 1 ) ) , if ( j < l , j , ( j + 1 ) ) >. ) ) ) )
Theorem	smatfval 29861*	Value of the submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.)
|- ( ( K e. NN /\ L e. NN /\ M e. V ) -> ( K (subMat1 ` M ) L ) = ( M o. ( i e. NN , j e. NN |-> <. if ( i < K , i , ( i + 1 ) ) , if ( j < L , j , ( j + 1 ) ) >. ) ) )
Theorem	smatrcl 29862	Closure of the rectangular submatrix. (Contributed by Thierry Arnoux, 19-Aug-2020.)
|- S = ( K (subMat1 ` A ) L )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> K e. ( 1 ... M ) )   &    |- ( ph -> L e. ( 1 ... N ) )   &    |- ( ph -> A e. ( B ^m ( ( 1 ... M ) X. ( 1 ... N ) ) ) )   =>    |- ( ph -> S e. ( B ^m ( ( 1 ... ( M - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) )
Theorem	smatlem 29863	Lemma for the next theorems. (Contributed by Thierry Arnoux, 19-Aug-2020.)
|- S = ( K (subMat1 ` A ) L )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> K e. ( 1 ... M ) )   &    |- ( ph -> L e. ( 1 ... N ) )   &    |- ( ph -> A e. ( B ^m ( ( 1 ... M ) X. ( 1 ... N ) ) ) )   &    |- ( ph -> I e. NN )   &    |- ( ph -> J e. NN )   &    |- ( ph -> if ( I < K , I , ( I + 1 ) ) = X )   &    |- ( ph -> if ( J < L , J , ( J + 1 ) ) = Y )   =>    |- ( ph -> ( I S J ) = ( X A Y ) )
Theorem	smattl 29864	Entries of a submatrix, top left. (Contributed by Thierry Arnoux, 19-Aug-2020.)
|- S = ( K (subMat1 ` A ) L )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> K e. ( 1 ... M ) )   &    |- ( ph -> L e. ( 1 ... N ) )   &    |- ( ph -> A e. ( B ^m ( ( 1 ... M ) X. ( 1 ... N ) ) ) )   &    |- ( ph -> I e. ( 1..^ K ) )   &    |- ( ph -> J e. ( 1..^ L ) )   =>    |- ( ph -> ( I S J ) = ( I A J ) )
Theorem	smattr 29865	Entries of a submatrix, top right. (Contributed by Thierry Arnoux, 19-Aug-2020.)
|- S = ( K (subMat1 ` A ) L )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> K e. ( 1 ... M ) )   &    |- ( ph -> L e. ( 1 ... N ) )   &    |- ( ph -> A e. ( B ^m ( ( 1 ... M ) X. ( 1 ... N ) ) ) )   &    |- ( ph -> I e. ( K ... M ) )   &    |- ( ph -> J e. ( 1..^ L ) )   =>    |- ( ph -> ( I S J ) = ( ( I + 1 ) A J ) )
Theorem	smatbl 29866	Entries of a submatrix, bottom left. (Contributed by Thierry Arnoux, 19-Aug-2020.)
|- S = ( K (subMat1 ` A ) L )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> K e. ( 1 ... M ) )   &    |- ( ph -> L e. ( 1 ... N ) )   &    |- ( ph -> A e. ( B ^m ( ( 1 ... M ) X. ( 1 ... N ) ) ) )   &    |- ( ph -> I e. ( 1..^ K ) )   &    |- ( ph -> J e. ( L ... N ) )   =>    |- ( ph -> ( I S J ) = ( I A ( J + 1 ) ) )
Theorem	smatbr 29867	Entries of a submatrix, bottom right. (Contributed by Thierry Arnoux, 19-Aug-2020.)
|- S = ( K (subMat1 ` A ) L )   &    |- ( ph -> M e. NN )   &    |- ( ph -> N e. NN )   &    |- ( ph -> K e. ( 1 ... M ) )   &    |- ( ph -> L e. ( 1 ... N ) )   &    |- ( ph -> A e. ( B ^m ( ( 1 ... M ) X. ( 1 ... N ) ) ) )   &    |- ( ph -> I e. ( K ... M ) )   &    |- ( ph -> J e. ( L ... N ) )   =>    |- ( ph -> ( I S J ) = ( ( I + 1 ) A ( J + 1 ) ) )
Theorem	smatcl 29868	Closure of the square submatrix: if M is a square matrix of dimension N with indexes in ( 1 ... N ), then a submatrix of M is of dimension ( N - 1 ). (Contributed by Thierry Arnoux, 19-Aug-2020.)
|- A = ( ( 1 ... N ) Mat R )   &    |- B = ( Base ` A )   &    |- C = ( Base ` ( ( 1 ... ( N - 1 ) ) Mat R ) )   &    |- S = ( K (subMat1 ` M ) L )   &    |- ( ph -> N e. NN )   &    |- ( ph -> K e. ( 1 ... N ) )   &    |- ( ph -> L e. ( 1 ... N ) )   &    |- ( ph -> M e. B )   =>    |- ( ph -> S e. C )
Theorem	matmpt2 29869*	Write a square matrix as a mapping operation. (Contributed by Thierry Arnoux, 16-Aug-2020.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   =>    |- ( M e. B -> M = ( i e. N , j e. N |-> ( i M j ) ) )
Theorem	1smat1 29870	The submatrix of the identity matrix obtained by removing the ith row and the ith column is an identity matrix. Cf. 1marepvsma1 20389. (Contributed by Thierry Arnoux, 19-Aug-2020.)
|- .1. = ( 1r ` ( ( 1 ... N ) Mat R ) )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> N e. NN )   &    |- ( ph -> I e. ( 1 ... N ) )   =>    |- ( ph -> ( I (subMat1 ` .1. ) I ) = ( 1r ` ( ( 1 ... ( N - 1 ) ) Mat R ) ) )
Theorem	submat1n 29871	One case where the submatrix with integer indices, subMat1, and the general submatrix subMat, agree. (Contributed by Thierry Arnoux, 22-Aug-2020.)
|- A = ( ( 1 ... N ) Mat R )   &    |- B = ( Base ` A )   =>    |- ( ( N e. NN /\ M e. B ) -> ( N (subMat1 ` M ) N ) = ( N ( ( ( 1 ... N ) subMat R ) ` M ) N ) )
Theorem	submatres 29872	Special case where the submatrix is a restriction of the initial matrix, and no renumbering occurs. (Contributed by Thierry Arnoux, 26-Aug-2020.)
|- A = ( ( 1 ... N ) Mat R )   &    |- B = ( Base ` A )   =>    |- ( ( N e. NN /\ M e. B ) -> ( N (subMat1 ` M ) N ) = ( M |` ( ( 1 ... ( N - 1 ) ) X. ( 1 ... ( N - 1 ) ) ) ) )
Theorem	submateqlem1 29873	Lemma for submateq 29875. (Contributed by Thierry Arnoux, 25-Aug-2020.)
|- ( ph -> N e. NN )   &    |- ( ph -> K e. ( 1 ... N ) )   &    |- ( ph -> M e. ( 1 ... ( N - 1 ) ) )   &    |- ( ph -> K <_ M )   =>    |- ( ph -> ( M e. ( K ... N ) /\ ( M + 1 ) e. ( ( 1 ... N ) \ { K } ) ) )
Theorem	submateqlem2 29874	Lemma for submateq 29875. (Contributed by Thierry Arnoux, 26-Aug-2020.)
|- ( ph -> N e. NN )   &    |- ( ph -> K e. ( 1 ... N ) )   &    |- ( ph -> M e. ( 1 ... ( N - 1 ) ) )   &    |- ( ph -> M < K )   =>    |- ( ph -> ( M e. ( 1..^ K ) /\ M e. ( ( 1 ... N ) \ { K } ) ) )
Theorem	submateq 29875*	Sufficient condition for two submatrices to be equal. (Contributed by Thierry Arnoux, 25-Aug-2020.)
|- A = ( ( 1 ... N ) Mat R )   &    |- B = ( Base ` A )   &    |- ( ph -> N e. NN )   &    |- ( ph -> I e. ( 1 ... N ) )   &    |- ( ph -> J e. ( 1 ... N ) )   &    |- ( ph -> E e. B )   &    |- ( ph -> F e. B )   &    |- ( ( ph /\ i e. ( ( 1 ... N ) \ { I } ) /\ j e. ( ( 1 ... N ) \ { J } ) ) -> ( i E j ) = ( i F j ) )   =>    |- ( ph -> ( I (subMat1 ` E ) J ) = ( I (subMat1 ` F ) J ) )
Theorem	submatminr1 29876	If we take a submatrix by removing the row I and column J, then the result is the same on the matrix with row I and column J modified by the minMatR1 operator. (Contributed by Thierry Arnoux, 25-Aug-2020.)
|- A = ( ( 1 ... N ) Mat R )   &    |- B = ( Base ` A )   &    |- ( ph -> N e. NN )   &    |- ( ph -> I e. ( 1 ... N ) )   &    |- ( ph -> J e. ( 1 ... N ) )   &    |- ( ph -> R e. Ring )   &    |- ( ph -> M e. B )   &    |- E = ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J )   =>    |- ( ph -> ( I (subMat1 ` M ) J ) = ( I (subMat1 ` E ) J ) )
20.3.10.5  Matrix literals
Syntax	clmat 29877	Extend class notation with the literal matrix conversion function.
class litMat
Definition	df-lmat 29878*	Define a function converting words of words into matrices. (Contributed by Thierry Arnoux, 28-Aug-2020.)
|- litMat = ( m e. _V |-> ( i e. ( 1 ... ( # ` m ) ) , j e. ( 1 ... ( # ` ( m ` 0 ) ) ) |-> ( ( m ` ( i - 1 ) ) ` ( j - 1 ) ) ) )
Theorem	lmatval 29879*	Value of the literal matrix conversion function. (Contributed by Thierry Arnoux, 28-Aug-2020.)
|- ( M e. V -> (litMat ` M ) = ( i e. ( 1 ... ( # ` M ) ) , j e. ( 1 ... ( # ` ( M ` 0 ) ) ) |-> ( ( M ` ( i - 1 ) ) ` ( j - 1 ) ) ) )
Theorem	lmatfval 29880*	Entries of a literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.)
|- M = (litMat ` W )   &    |- ( ph -> N e. NN )   &    |- ( ph -> W e. Word Word V )   &    |- ( ph -> ( # ` W ) = N )   &    |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( # ` ( W ` i ) ) = N )   &    |- ( ph -> I e. ( 1 ... N ) )   &    |- ( ph -> J e. ( 1 ... N ) )   =>    |- ( ph -> ( I M J ) = ( ( W ` ( I - 1 ) ) ` ( J - 1 ) ) )
Theorem	lmatfvlem 29881*	Useful lemma to extract literal matrix entries. Suggested by Mario Carneiro. (Contributed by Thierry Arnoux, 3-Sep-2020.)
|- M = (litMat ` W )   &    |- ( ph -> N e. NN )   &    |- ( ph -> W e. Word Word V )   &    |- ( ph -> ( # ` W ) = N )   &    |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( # ` ( W ` i ) ) = N )   &    |- K e. NN0   &    |- L e. NN0   &    |- I <_ N   &    |- J <_ N   &    |- ( K + 1 ) = I   &    |- ( L + 1 ) = J   &    |- ( W ` K ) = X   &    |- ( ph -> ( X ` L ) = Y )   =>    |- ( ph -> ( I M J ) = Y )
Theorem	lmatcl 29882*	Closure of the literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.)
|- M = (litMat ` W )   &    |- ( ph -> N e. NN )   &    |- ( ph -> W e. Word Word V )   &    |- ( ph -> ( # ` W ) = N )   &    |- ( ( ph /\ i e. ( 0..^ N ) ) -> ( # ` ( W ` i ) ) = N )   &    |- V = ( Base ` R )   &    |- O = ( ( 1 ... N ) Mat R )   &    |- P = ( Base ` O )   &    |- ( ph -> R e. X )   =>    |- ( ph -> M e. P )
Theorem	lmat22lem 29883*	Lemma for lmat22e11 29884 and co. (Contributed by Thierry Arnoux, 28-Aug-2020.)
|- M = (litMat ` <" <" A B "> <" C D "> "> )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ( ph /\ i e. ( 0..^ 2 ) ) -> ( # ` ( <" <" A B "> <" C D "> "> ` i ) ) = 2 )
Theorem	lmat22e11 29884	Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 28-Aug-2020.)
|- M = (litMat ` <" <" A B "> <" C D "> "> )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ph -> ( 1 M 1 ) = A )
Theorem	lmat22e12 29885	Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.)
|- M = (litMat ` <" <" A B "> <" C D "> "> )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ph -> ( 1 M 2 ) = B )
Theorem	lmat22e21 29886	Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.)
|- M = (litMat ` <" <" A B "> <" C D "> "> )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ph -> ( 2 M 1 ) = C )
Theorem	lmat22e22 29887	Entry of a 2x2 literal matrix. (Contributed by Thierry Arnoux, 12-Sep-2020.)
|- M = (litMat ` <" <" A B "> <" C D "> "> )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   =>    |- ( ph -> ( 2 M 2 ) = D )
Theorem	lmat22det 29888	The determinant of a literal 2x2 complex matrix. (Contributed by Thierry Arnoux, 1-Sep-2020.)
|- M = (litMat ` <" <" A B "> <" C D "> "> )   &    |- ( ph -> A e. V )   &    |- ( ph -> B e. V )   &    |- ( ph -> C e. V )   &    |- ( ph -> D e. V )   &    |- .x. = ( .r ` R )   &    |- .- = ( -g ` R )   &    |- V = ( Base ` R )   &    |- J = ( ( 1 ... 2 ) maDet R )   &    |- ( ph -> R e. Ring )   =>    |- ( ph -> ( J ` M ) = ( ( A .x. D ) .- ( C .x. B ) ) )
20.3.10.6  Laplace expansion of determinants
Theorem	mdetpmtr1 29889*	The determinant of a matrix with permuted rows is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- D = ( N maDet R )   &    |- G = ( Base ` ( SymGrp ` N ) )   &    |- S = (pmSgn ` N )   &    |- Z = ( ZRHom ` R )   &    |- .x. = ( .r ` R )   &    |- E = ( i e. N , j e. N |-> ( ( P ` i ) M j ) )   =>    |- ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` M ) = ( ( ( Z o. S ) ` P ) .x. ( D ` E ) ) )
Theorem	mdetpmtr2 29890*	The determinant of a matrix with permuted columns is the determinant of the original matrix multiplied by the sign of the permutation. (Contributed by Thierry Arnoux, 22-Aug-2020.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- D = ( N maDet R )   &    |- G = ( Base ` ( SymGrp ` N ) )   &    |- S = (pmSgn ` N )   &    |- Z = ( ZRHom ` R )   &    |- .x. = ( .r ` R )   &    |- E = ( i e. N , j e. N |-> ( i M ( P ` j ) ) )   =>    |- ( ( ( R e. CRing /\ N e. Fin ) /\ ( M e. B /\ P e. G ) ) -> ( D ` M ) = ( ( ( Z o. S ) ` P ) .x. ( D ` E ) ) )
Theorem	mdetpmtr12 29891*	The determinant of a matrix with permuted rows and columns is the determinant of the original matrix multiplied by the product of the signs of the permutations. (Contributed by Thierry Arnoux, 22-Aug-2020.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- D = ( N maDet R )   &    |- G = ( Base ` ( SymGrp ` N ) )   &    |- S = (pmSgn ` N )   &    |- Z = ( ZRHom ` R )   &    |- .x. = ( .r ` R )   &    |- E = ( i e. N , j e. N |-> ( ( P ` i ) M ( Q ` j ) ) )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> N e. Fin )   &    |- ( ph -> M e. B )   &    |- ( ph -> P e. G )   &    |- ( ph -> Q e. G )   =>    |- ( ph -> ( D ` M ) = ( ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) .x. ( D ` E ) ) )
Theorem	mdetlap1 29892*	A Laplace expansion of the determinant of a matrix, using the adjunct (cofactor) matrix. (Contributed by Thierry Arnoux, 16-Aug-2020.)
|- A = ( N Mat R )   &    |- B = ( Base ` A )   &    |- D = ( N maDet R )   &    |- K = ( N maAdju R )   &    |- .x. = ( .r ` R )   =>    |- ( ( R e. CRing /\ M e. B /\ I e. N ) -> ( D ` M ) = ( R gsumg ( j e. N |-> ( ( I M j ) .x. ( j ( K ` M ) I ) ) ) ) )
Theorem	madjusmdetlem1 29893*	Lemma for madjusmdet 29897. (Contributed by Thierry Arnoux, 22-Aug-2020.)
|- B = ( Base ` A )   &    |- A = ( ( 1 ... N ) Mat R )   &    |- D = ( ( 1 ... N ) maDet R )   &    |- K = ( ( 1 ... N ) maAdju R )   &    |- .x. = ( .r ` R )   &    |- Z = ( ZRHom ` R )   &    |- E = ( ( 1 ... ( N - 1 ) ) maDet R )   &    |- ( ph -> N e. NN )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> I e. ( 1 ... N ) )   &    |- ( ph -> J e. ( 1 ... N ) )   &    |- ( ph -> M e. B )   &    |- G = ( Base ` ( SymGrp ` ( 1 ... N ) ) )   &    |- S = (pmSgn ` ( 1 ... N ) )   &    |- U = ( I ( ( ( 1 ... N ) minMatR1 R ) ` M ) J )   &    |- W = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( P ` i ) U ( Q ` j ) ) )   &    |- ( ph -> P e. G )   &    |- ( ph -> Q e. G )   &    |- ( ph -> ( P ` N ) = I )   &    |- ( ph -> ( Q ` N ) = J )   &    |- ( ph -> ( I (subMat1 ` U ) J ) = ( N (subMat1 ` W ) N ) )   =>    |- ( ph -> ( J ( K ` M ) I ) = ( ( Z ` ( ( S ` P ) x. ( S ` Q ) ) ) .x. ( E ` ( I (subMat1 ` M ) J ) ) ) )
Theorem	madjusmdetlem2 29894*	Lemma for madjusmdet 29897. (Contributed by Thierry Arnoux, 26-Aug-2020.)
|- B = ( Base ` A )   &    |- A = ( ( 1 ... N ) Mat R )   &    |- D = ( ( 1 ... N ) maDet R )   &    |- K = ( ( 1 ... N ) maAdju R )   &    |- .x. = ( .r ` R )   &    |- Z = ( ZRHom ` R )   &    |- E = ( ( 1 ... ( N - 1 ) ) maDet R )   &    |- ( ph -> N e. NN )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> I e. ( 1 ... N ) )   &    |- ( ph -> J e. ( 1 ... N ) )   &    |- ( ph -> M e. B )   &    |- P = ( i e. ( 1 ... N ) |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )   &    |- S = ( i e. ( 1 ... N ) |-> if ( i = 1 , N , if ( i <_ N , ( i - 1 ) , i ) ) )   =>    |- ( ( ph /\ X e. ( 1 ... ( N - 1 ) ) ) -> if ( X < I , X , ( X + 1 ) ) = ( ( P o. `' S ) ` X ) )
Theorem	madjusmdetlem3 29895*	Lemma for madjusmdet 29897. (Contributed by Thierry Arnoux, 27-Aug-2020.)
|- B = ( Base ` A )   &    |- A = ( ( 1 ... N ) Mat R )   &    |- D = ( ( 1 ... N ) maDet R )   &    |- K = ( ( 1 ... N ) maAdju R )   &    |- .x. = ( .r ` R )   &    |- Z = ( ZRHom ` R )   &    |- E = ( ( 1 ... ( N - 1 ) ) maDet R )   &    |- ( ph -> N e. NN )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> I e. ( 1 ... N ) )   &    |- ( ph -> J e. ( 1 ... N ) )   &    |- ( ph -> M e. B )   &    |- P = ( i e. ( 1 ... N ) |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )   &    |- S = ( i e. ( 1 ... N ) |-> if ( i = 1 , N , if ( i <_ N , ( i - 1 ) , i ) ) )   &    |- Q = ( j e. ( 1 ... N ) |-> if ( j = 1 , J , if ( j <_ J , ( j - 1 ) , j ) ) )   &    |- T = ( j e. ( 1 ... N ) |-> if ( j = 1 , N , if ( j <_ N , ( j - 1 ) , j ) ) )   &    |- W = ( i e. ( 1 ... N ) , j e. ( 1 ... N ) |-> ( ( ( P o. `' S ) ` i ) U ( ( Q o. `' T ) ` j ) ) )   &    |- ( ph -> U e. B )   =>    |- ( ph -> ( I (subMat1 ` U ) J ) = ( N (subMat1 ` W ) N ) )
Theorem	madjusmdetlem4 29896*	Lemma for madjusmdet 29897. (Contributed by Thierry Arnoux, 22-Aug-2020.)
|- B = ( Base ` A )   &    |- A = ( ( 1 ... N ) Mat R )   &    |- D = ( ( 1 ... N ) maDet R )   &    |- K = ( ( 1 ... N ) maAdju R )   &    |- .x. = ( .r ` R )   &    |- Z = ( ZRHom ` R )   &    |- E = ( ( 1 ... ( N - 1 ) ) maDet R )   &    |- ( ph -> N e. NN )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> I e. ( 1 ... N ) )   &    |- ( ph -> J e. ( 1 ... N ) )   &    |- ( ph -> M e. B )   &    |- P = ( i e. ( 1 ... N ) |-> if ( i = 1 , I , if ( i <_ I , ( i - 1 ) , i ) ) )   &    |- S = ( i e. ( 1 ... N ) |-> if ( i = 1 , N , if ( i <_ N , ( i - 1 ) , i ) ) )   &    |- Q = ( j e. ( 1 ... N ) |-> if ( j = 1 , J , if ( j <_ J , ( j - 1 ) , j ) ) )   &    |- T = ( j e. ( 1 ... N ) |-> if ( j = 1 , N , if ( j <_ N , ( j - 1 ) , j ) ) )   =>    |- ( ph -> ( J ( K ` M ) I ) = ( ( Z ` ( -u 1 ^ ( I + J ) ) ) .x. ( E ` ( I (subMat1 ` M ) J ) ) ) )
Theorem	madjusmdet 29897	Express the cofactor of the matrix, i.e. the entries of its adjunct matrix, using determinant of submatrixes. (Contributed by Thierry Arnoux, 23-Aug-2020.)
|- B = ( Base ` A )   &    |- A = ( ( 1 ... N ) Mat R )   &    |- D = ( ( 1 ... N ) maDet R )   &    |- K = ( ( 1 ... N ) maAdju R )   &    |- .x. = ( .r ` R )   &    |- Z = ( ZRHom ` R )   &    |- E = ( ( 1 ... ( N - 1 ) ) maDet R )   &    |- ( ph -> N e. NN )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> I e. ( 1 ... N ) )   &    |- ( ph -> J e. ( 1 ... N ) )   &    |- ( ph -> M e. B )   =>    |- ( ph -> ( J ( K ` M ) I ) = ( ( Z ` ( -u 1 ^ ( I + J ) ) ) .x. ( E ` ( I (subMat1 ` M ) J ) ) ) )
Theorem	mdetlap 29898*	Laplace expansion of the determinant of a square matrix. (Contributed by Thierry Arnoux, 19-Aug-2020.)
|- B = ( Base ` A )   &    |- A = ( ( 1 ... N ) Mat R )   &    |- D = ( ( 1 ... N ) maDet R )   &    |- K = ( ( 1 ... N ) maAdju R )   &    |- .x. = ( .r ` R )   &    |- Z = ( ZRHom ` R )   &    |- E = ( ( 1 ... ( N - 1 ) ) maDet R )   &    |- ( ph -> N e. NN )   &    |- ( ph -> R e. CRing )   &    |- ( ph -> I e. ( 1 ... N ) )   &    |- ( ph -> J e. ( 1 ... N ) )   &    |- ( ph -> M e. B )   =>    |- ( ph -> ( D ` M ) = ( R gsumg ( j e. ( 1 ... N ) |-> ( ( Z ` ( -u 1 ^ ( I + j ) ) ) .x. ( ( I M j ) .x. ( E ` ( I (subMat1 ` M ) j ) ) ) ) ) ) )
20.3.11  Topology
20.3.11.1  Open maps
Theorem	fvproj 29899*	Value of a function on pairs, given two projections F and G. (Contributed by Thierry Arnoux, 30-Dec-2019.)
|- H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. )   &    |- ( ph -> X e. A )   &    |- ( ph -> Y e. B )   =>    |- ( ph -> ( H ` <. X , Y >. ) = <. ( F ` X ) , ( G ` Y ) >. )
Theorem	fimaproj 29900*	Image of a cartesian product for a function on pairs, given two projections F and G. (Contributed by Thierry Arnoux, 30-Dec-2019.)
|- H = ( x e. A , y e. B |-> <. ( F ` x ) , ( G ` y ) >. )   &    |- ( ph -> F Fn A )   &    |- ( ph -> G Fn B )   &    |- ( ph -> X C_ A )   &    |- ( ph -> Y C_ B )   =>    |- ( ph -> ( H " ( X X. Y ) ) = ( ( F " X ) X. ( G " Y ) ) )