Here is, as promised, the corrected theorem and related basic theorems,
checked by metamath.exe as well as mmj2. Theorem qfrm was added, which
charaterizes the set of quadratic forms over a set/vector space V. See the
remarks in its comment about the necessity of V to be a set. Of course, the
bilinearity has to be added, as described by Thierry.
${
$d a q v w $.
$( The definition of a "quadratic form". (Contributed by ...,
5-Feb-2022.) $)
df-qfrm $a |- QFrm = ( w e. _V
|-> { q e. ( ( Base ` ( Scalar ` w ) ) ^m ( Base ` w ) ) |
A. v e. ( Base ` w ) A. a e. ( Base ` ( Scalar ` w ) )
( q ` ( a ( .s ` w ) v ) )
= ( ( a ( .r ` ( Scalar ` w ) ) a ) ( .s ` w ) ( q ` v ) ) }
) $.
$}
${
$d B q w $. $d K q w $. $d U w $. $d V a q v w $. $d .x. w $.
$d .X. w $.
qfrm.b $e |- B = ( Base ` V ) $.
qfrm.m $e |- .x. = ( .s ` V ) $.
qfrm.s $e |- S = ( Scalar ` V ) $.
qfrm.k $e |- K = ( Base ` S ) $.
qfrm.t $e |- .X. = ( .r ` S ) $.
$( The set of quadratic forms over a set ` V `. The assumption that `
V `
must be a set (` V e. U `) is necessary, because if ` V ` was a
proper
class (` V e/ _V `) , then ` ( QFrm `` V ) = (/) ` (see ~ fvprc ),
but
the right hand side of the equation would be ` { (/) } =/= (/) `
(see ~ mapdm0 and ~ ral0 ). Usually, ` V ` will be a vector space
(` U = LVec `, i.e. ` V e. LVec `). (Contributed by ...,
5-Feb-2022.) $)
qfrm $p |- ( V e. U -> ( QFrm ` V ) = { q e. ( K ^m B ) |
A. v e. B A. a e. K
( q ` ( a .x. v ) ) = ( ( a .X. a ) .x. ( q ` v ) ) }
) $=
? $.
$d Q a q v $. $d .x. q $. $d .X. q $.
$( The predicate "is a quadratic form". (Contributed by ...,
5-Feb-2022.) $)
isqfrm $p |- ( V e. U -> ( Q e. ( QFrm ` V ) <-> ( Q e. ( K ^m B )
/\ A. v e. B A. a e. K
( Q ` ( a .x. v ) ) = ( ( a .X. a ) .x. ( Q ` v ) ) ) )
) $=
? $.
$( A quadratic form is a function from a class ` B ` (usually the base
set
of a vector space) to the base set ` K ` of its scalars ` S `
(usually a
field). (Contributed by ..., 5-Feb-2022.) $)
qfrmf $p |- ( Q e. ( QFrm ` V ) -> Q : B --> K ) $=
? $.
$d A a $. $d B v $. $d K a v $. $d Q a v $. $d X a v $.
$d .x. a v $. $d .X. a v $.
$( The property of a quadratic form as a function from a class ` V `
(usually a vector space) to its scalars ` S ` (usually a field).
(Contributed by ..., 5-Feb-2022.) $)
qfrmprop $p |- ( ( Q e. ( QFrm ` V ) /\ X e. B /\ A e. K )
-> ( Q ` ( A .x. X ) ) = ( ( A .X. A ) .x. ( Q ` X ) )
) $=
? $.
$}
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/77fa41cd-abe8-4a55-b10b-2a838d7440e4n%40googlegroups.com.
