Proof of proveit.linear_algebra.scalar_multiplication.scalar_mult_eq theorem

import proveit
theory = proveit.Theory() # the theorem's theory
from proveit import defaults
from proveit import x, alpha
from proveit.linear_algebra import ScalarMult

%proving scalar_mult_eq

With these allowed/disallowed theorem/theory presumptions (e.g., to avoid circular dependencies), we begin our proof of
scalar_mult_eq:
(see dependencies)

defaults.assumptions = scalar_mult_eq.all_conditions()

defaults.assumptions:

x_eq_y = defaults.assumptions[-1]

x_eq_y:

x_eq_y.substitution(ScalarMult(alpha, x))

 ⊢  

scalar_mult_eq may now be readily provable (assuming required theorems are usable).  Simply execute "%qed".

%qed

proveit.linear_algebra.scalar_multiplication.scalar_mult_eq has been proven.

	step type	requirements	statement
0	generalization	1	⊢
1	instantiation	2, 3	⊢
	: , : , :
2	axiom		⊢
	proveit.logic.equality.substitution
3	assumption		⊢