isslmd

Description: The predicate "is a semimodule". (Contributed by NM, 4-Nov-2013) (Revised by Mario Carneiro, 19-Jun-2014) (Revised by Thierry Arnoux, 1-Apr-2018)

	Ref	Expression
Hypotheses	isslmd.v	$⊢ V = {Base}_{W}$
	isslmd.a	$⊢ \underset{˙}{+} = +_{W}$
	isslmd.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	isslmd.0	$⊢ \underset{˙}{0} = 0_{W}$
	isslmd.f	$⊢ F = Scalar (W)$
	isslmd.k	$⊢ K = {Base}_{F}$
	isslmd.p	$⊢ \underset{˙}{⨣} = +_{F}$
	isslmd.t	$⊢ \underset{˙}{\times} = \cdot_{F}$
	isslmd.u	$⊢ \underset{˙}{1} = 1_{F}$
	isslmd.o	$⊢ O = 0_{F}$
Assertion	isslmd	$⊢ W \in SLMod \leftrightarrow (W \in CMnd \land F \in SRing \land \forall q \in K \forall r \in K \forall x \in V \forall w \in V ((r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)) \land ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0})))$

Proof

Step	Hyp	Ref	Expression
1		isslmd.v	$⊢ V = {Base}_{W}$
2		isslmd.a	$⊢ \underset{˙}{+} = +_{W}$
3		isslmd.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
4		isslmd.0	$⊢ \underset{˙}{0} = 0_{W}$
5		isslmd.f	$⊢ F = Scalar (W)$
6		isslmd.k	$⊢ K = {Base}_{F}$
7		isslmd.p	$⊢ \underset{˙}{⨣} = +_{F}$
8		isslmd.t	$⊢ \underset{˙}{\times} = \cdot_{F}$
9		isslmd.u	$⊢ \underset{˙}{1} = 1_{F}$
10		isslmd.o	$⊢ O = 0_{F}$
11		fvex	$⊢ {Base}_{g} \in V$
12		fvex	$⊢ +_{g} \in V$
13		fvex	$⊢ \cdot_{g} \in V$
14		fvex	$⊢ Scalar (g) \in V$
15		fvex	$⊢ {Base}_{f} \in V$
16		fvex	$⊢ +_{f} \in V$
17		fvex	$⊢ \cdot_{f} \in V$
18		simp1	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to k = {Base}_{f}$
19		simp2	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to p = +_{f}$
20	19	oveqd	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to q p r = q +_{f} r$
21	20	oveq1d	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to (q p r) s w = (q +_{f} r) s w$
22	21	eqeq1d	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to ((q p r) s w = (q s w) a (r s w) \leftrightarrow (q +_{f} r) s w = (q s w) a (r s w))$
23	22	3anbi3d	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \leftrightarrow (r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)))$
24		simp3	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to t = \cdot_{f}$
25	24	oveqd	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to q t r = q \cdot_{f} r$
26	25	oveq1d	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to (q t r) s w = (q \cdot_{f} r) s w$
27	26	eqeq1d	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to ((q t r) s w = q s (r s w) \leftrightarrow (q \cdot_{f} r) s w = q s (r s w))$
28	27	3anbi1d	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to (((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g}) \leftrightarrow ((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g}))$
29	23 28	anbi12d	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to (((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \land ((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})) \leftrightarrow ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)) \land ((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})))$
30	29	2ralbidv	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to (\forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \land ((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})) \leftrightarrow \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)) \land ((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})))$
31	18 30	raleqbidv	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to (\forall r \in k \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \land ((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})) \leftrightarrow \forall r \in {Base}_{f} \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)) \land ((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})))$
32	18 31	raleqbidv	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to (\forall q \in k \forall r \in k \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \land ((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})) \leftrightarrow \forall q \in {Base}_{f} \forall r \in {Base}_{f} \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)) \land ((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})))$
33	32	anbi2d	$⊢ (k = {Base}_{f} \land p = +_{f} \land t = \cdot_{f}) \to ((f \in SRing \land \forall q \in k \forall r \in k \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \land ((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g}))) \leftrightarrow (f \in SRing \land \forall q \in {Base}_{f} \forall r \in {Base}_{f} \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)) \land ((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g}))))$
34	15 16 17 33	sbc3ie	$⊢ \underset{˙}{[} {Base}_{f} / k \underset{˙}{]} \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} (f \in SRing \land \forall q \in k \forall r \in k \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \land ((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g}))) \leftrightarrow (f \in SRing \land \forall q \in {Base}_{f} \forall r \in {Base}_{f} \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)) \land ((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})))$
35		simpr	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to f = Scalar (g)$
36	35	eleq1d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (f \in SRing \leftrightarrow Scalar (g) \in SRing)$
37	35	fveq2d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to {Base}_{f} = {Base}_{Scalar (g)}$
38		simpl	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to s = \cdot_{g}$
39	38	oveqd	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to r s w = r \cdot_{g} w$
40	39	eleq1d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (r s w \in v \leftrightarrow r \cdot_{g} w \in v)$
41	38	oveqd	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to r s (w a x) = r \cdot_{g} (w a x)$
42	38	oveqd	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to r s x = r \cdot_{g} x$
43	39 42	oveq12d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (r s w) a (r s x) = (r \cdot_{g} w) a (r \cdot_{g} x)$
44	41 43	eqeq12d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (r s (w a x) = (r s w) a (r s x) \leftrightarrow r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x))$
45	35	fveq2d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to +_{f} = +_{Scalar (g)}$
46	45	oveqd	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to q +_{f} r = q +_{Scalar (g)} r$
47		eqidd	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to w = w$
48	38 46 47	oveq123d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (q +_{f} r) s w = (q +_{Scalar (g)} r) \cdot_{g} w$
49	38	oveqd	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to q s w = q \cdot_{g} w$
50	49 39	oveq12d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (q s w) a (r s w) = (q \cdot_{g} w) a (r \cdot_{g} w)$
51	48 50	eqeq12d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to ((q +_{f} r) s w = (q s w) a (r s w) \leftrightarrow (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w))$
52	40 44 51	3anbi123d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)) \leftrightarrow (r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)))$
53	35	fveq2d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to \cdot_{f} = \cdot_{Scalar (g)}$
54	53	oveqd	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to q \cdot_{f} r = q \cdot_{Scalar (g)} r$
55	38 54 47	oveq123d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (q \cdot_{f} r) s w = (q \cdot_{Scalar (g)} r) \cdot_{g} w$
56		eqidd	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to q = q$
57	38 56 39	oveq123d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to q s (r s w) = q \cdot_{g} (r \cdot_{g} w)$
58	55 57	eqeq12d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to ((q \cdot_{f} r) s w = q s (r s w) \leftrightarrow (q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w))$
59	35	fveq2d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to 1_{f} = 1_{Scalar (g)}$
60	38 59 47	oveq123d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to 1_{f} s w = 1_{Scalar (g)} \cdot_{g} w$
61	60	eqeq1d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (1_{f} s w = w \leftrightarrow 1_{Scalar (g)} \cdot_{g} w = w)$
62	35	fveq2d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to 0_{f} = 0_{Scalar (g)}$
63	38 62 47	oveq123d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to 0_{f} s w = 0_{Scalar (g)} \cdot_{g} w$
64	63	eqeq1d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (0_{f} s w = 0_{g} \leftrightarrow 0_{Scalar (g)} \cdot_{g} w = 0_{g})$
65	58 61 64	3anbi123d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g}) \leftrightarrow ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g}))$
66	52 65	anbi12d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)) \land ((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})) \leftrightarrow ((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})))$
67	66	2ralbidv	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (\forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)) \land ((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})) \leftrightarrow \forall x \in v \forall w \in v ((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})))$
68	37 67	raleqbidv	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (\forall r \in {Base}_{f} \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)) \land ((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})) \leftrightarrow \forall r \in {Base}_{Scalar (g)} \forall x \in v \forall w \in v ((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})))$
69	37 68	raleqbidv	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (\forall q \in {Base}_{f} \forall r \in {Base}_{f} \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)) \land ((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})) \leftrightarrow \forall q \in {Base}_{Scalar (g)} \forall r \in {Base}_{Scalar (g)} \forall x \in v \forall w \in v ((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})))$
70	36 69	anbi12d	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to ((f \in SRing \land \forall q \in {Base}_{f} \forall r \in {Base}_{f} \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q +_{f} r) s w = (q s w) a (r s w)) \land ((q \cdot_{f} r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g}))) \leftrightarrow (Scalar (g) \in SRing \land \forall q \in {Base}_{Scalar (g)} \forall r \in {Base}_{Scalar (g)} \forall x \in v \forall w \in v ((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g}))))$
71	34 70	syl5bb	$⊢ (s = \cdot_{g} \land f = Scalar (g)) \to (\underset{˙}{[} {Base}_{f} / k \underset{˙}{]} \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} (f \in SRing \land \forall q \in k \forall r \in k \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \land ((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g}))) \leftrightarrow (Scalar (g) \in SRing \land \forall q \in {Base}_{Scalar (g)} \forall r \in {Base}_{Scalar (g)} \forall x \in v \forall w \in v ((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g}))))$
72	13 14 71	sbc2ie	$⊢ \underset{˙}{[} \cdot_{g} / s \underset{˙}{]} \underset{˙}{[} Scalar (g) / f \underset{˙}{]} \underset{˙}{[} {Base}_{f} / k \underset{˙}{]} \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} (f \in SRing \land \forall q \in k \forall r \in k \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \land ((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g}))) \leftrightarrow (Scalar (g) \in SRing \land \forall q \in {Base}_{Scalar (g)} \forall r \in {Base}_{Scalar (g)} \forall x \in v \forall w \in v ((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})))$
73		simpl	$⊢ (v = {Base}_{g} \land a = +_{g}) \to v = {Base}_{g}$
74	73	eleq2d	$⊢ (v = {Base}_{g} \land a = +_{g}) \to (r \cdot_{g} w \in v \leftrightarrow r \cdot_{g} w \in {Base}_{g})$
75		simpr	$⊢ (v = {Base}_{g} \land a = +_{g}) \to a = +_{g}$
76	75	oveqd	$⊢ (v = {Base}_{g} \land a = +_{g}) \to w a x = w +_{g} x$
77	76	oveq2d	$⊢ (v = {Base}_{g} \land a = +_{g}) \to r \cdot_{g} (w a x) = r \cdot_{g} (w +_{g} x)$
78	75	oveqd	$⊢ (v = {Base}_{g} \land a = +_{g}) \to (r \cdot_{g} w) a (r \cdot_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x)$
79	77 78	eqeq12d	$⊢ (v = {Base}_{g} \land a = +_{g}) \to (r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \leftrightarrow r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x))$
80	75	oveqd	$⊢ (v = {Base}_{g} \land a = +_{g}) \to (q \cdot_{g} w) a (r \cdot_{g} w) = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)$
81	80	eqeq2d	$⊢ (v = {Base}_{g} \land a = +_{g}) \to ((q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w) \leftrightarrow (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w))$
82	74 79 81	3anbi123d	$⊢ (v = {Base}_{g} \land a = +_{g}) \to ((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \leftrightarrow (r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)))$
83	82	anbi1d	$⊢ (v = {Base}_{g} \land a = +_{g}) \to (((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})) \leftrightarrow ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})))$
84	73 83	raleqbidv	$⊢ (v = {Base}_{g} \land a = +_{g}) \to (\forall w \in v ((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})) \leftrightarrow \forall w \in {Base}_{g} ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})))$
85	73 84	raleqbidv	$⊢ (v = {Base}_{g} \land a = +_{g}) \to (\forall x \in v \forall w \in v ((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})) \leftrightarrow \forall x \in {Base}_{g} \forall w \in {Base}_{g} ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})))$
86	85	2ralbidv	$⊢ (v = {Base}_{g} \land a = +_{g}) \to (\forall q \in {Base}_{Scalar (g)} \forall r \in {Base}_{Scalar (g)} \forall x \in v \forall w \in v ((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})) \leftrightarrow \forall q \in {Base}_{Scalar (g)} \forall r \in {Base}_{Scalar (g)} \forall x \in {Base}_{g} \forall w \in {Base}_{g} ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})))$
87	86	anbi2d	$⊢ (v = {Base}_{g} \land a = +_{g}) \to ((Scalar (g) \in SRing \land \forall q \in {Base}_{Scalar (g)} \forall r \in {Base}_{Scalar (g)} \forall x \in v \forall w \in v ((r \cdot_{g} w \in v \land r \cdot_{g} (w a x) = (r \cdot_{g} w) a (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) a (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g}))) \leftrightarrow (Scalar (g) \in SRing \land \forall q \in {Base}_{Scalar (g)} \forall r \in {Base}_{Scalar (g)} \forall x \in {Base}_{g} \forall w \in {Base}_{g} ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g}))))$
88	72 87	syl5bb	$⊢ (v = {Base}_{g} \land a = +_{g}) \to (\underset{˙}{[} \cdot_{g} / s \underset{˙}{]} \underset{˙}{[} Scalar (g) / f \underset{˙}{]} \underset{˙}{[} {Base}_{f} / k \underset{˙}{]} \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} (f \in SRing \land \forall q \in k \forall r \in k \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \land ((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g}))) \leftrightarrow (Scalar (g) \in SRing \land \forall q \in {Base}_{Scalar (g)} \forall r \in {Base}_{Scalar (g)} \forall x \in {Base}_{g} \forall w \in {Base}_{g} ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g}))))$
89	11 12 88	sbc2ie	$⊢ \underset{˙}{[} {Base}_{g} / v \underset{˙}{]} \underset{˙}{[} +_{g} / a \underset{˙}{]} \underset{˙}{[} \cdot_{g} / s \underset{˙}{]} \underset{˙}{[} Scalar (g) / f \underset{˙}{]} \underset{˙}{[} {Base}_{f} / k \underset{˙}{]} \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} (f \in SRing \land \forall q \in k \forall r \in k \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \land ((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g}))) \leftrightarrow (Scalar (g) \in SRing \land \forall q \in {Base}_{Scalar (g)} \forall r \in {Base}_{Scalar (g)} \forall x \in {Base}_{g} \forall w \in {Base}_{g} ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})))$
90		fveq2	$⊢ g = W \to Scalar (g) = Scalar (W)$
91	90 5	eqtr4di	$⊢ g = W \to Scalar (g) = F$
92	91	eleq1d	$⊢ g = W \to (Scalar (g) \in SRing \leftrightarrow F \in SRing)$
93	91	fveq2d	$⊢ g = W \to {Base}_{Scalar (g)} = {Base}_{F}$
94	93 6	eqtr4di	$⊢ g = W \to {Base}_{Scalar (g)} = K$
95		fveq2	$⊢ g = W \to {Base}_{g} = {Base}_{W}$
96	95 1	eqtr4di	$⊢ g = W \to {Base}_{g} = V$
97		fveq2	$⊢ g = W \to \cdot_{g} = \cdot_{W}$
98	97 3	eqtr4di	$⊢ g = W \to \cdot_{g} = \underset{˙}{\cdot}$
99	98	oveqd	$⊢ g = W \to r \cdot_{g} w = r \underset{˙}{\cdot} w$
100	99 96	eleq12d	$⊢ g = W \to (r \cdot_{g} w \in {Base}_{g} \leftrightarrow r \underset{˙}{\cdot} w \in V)$
101		eqidd	$⊢ g = W \to r = r$
102		fveq2	$⊢ g = W \to +_{g} = +_{W}$
103	102 2	eqtr4di	$⊢ g = W \to +_{g} = \underset{˙}{+}$
104	103	oveqd	$⊢ g = W \to w +_{g} x = w \underset{˙}{+} x$
105	98 101 104	oveq123d	$⊢ g = W \to r \cdot_{g} (w +_{g} x) = r \underset{˙}{\cdot} (w \underset{˙}{+} x)$
106	98	oveqd	$⊢ g = W \to r \cdot_{g} x = r \underset{˙}{\cdot} x$
107	103 99 106	oveq123d	$⊢ g = W \to (r \cdot_{g} w) +_{g} (r \cdot_{g} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x)$
108	105 107	eqeq12d	$⊢ g = W \to (r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \leftrightarrow r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x))$
109	91	fveq2d	$⊢ g = W \to +_{Scalar (g)} = +_{F}$
110	109 7	eqtr4di	$⊢ g = W \to +_{Scalar (g)} = \underset{˙}{⨣}$
111	110	oveqd	$⊢ g = W \to q +_{Scalar (g)} r = q \underset{˙}{⨣} r$
112		eqidd	$⊢ g = W \to w = w$
113	98 111 112	oveq123d	$⊢ g = W \to (q +_{Scalar (g)} r) \cdot_{g} w = (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w$
114	98	oveqd	$⊢ g = W \to q \cdot_{g} w = q \underset{˙}{\cdot} w$
115	103 114 99	oveq123d	$⊢ g = W \to (q \cdot_{g} w) +_{g} (r \cdot_{g} w) = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)$
116	113 115	eqeq12d	$⊢ g = W \to ((q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w) \leftrightarrow (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w))$
117	100 108 116	3anbi123d	$⊢ g = W \to ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \leftrightarrow (r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)))$
118	91	fveq2d	$⊢ g = W \to \cdot_{Scalar (g)} = \cdot_{F}$
119	118 8	eqtr4di	$⊢ g = W \to \cdot_{Scalar (g)} = \underset{˙}{\times}$
120	119	oveqd	$⊢ g = W \to q \cdot_{Scalar (g)} r = q \underset{˙}{\times} r$
121	98 120 112	oveq123d	$⊢ g = W \to (q \cdot_{Scalar (g)} r) \cdot_{g} w = (q \underset{˙}{\times} r) \underset{˙}{\cdot} w$
122		eqidd	$⊢ g = W \to q = q$
123	98 122 99	oveq123d	$⊢ g = W \to q \cdot_{g} (r \cdot_{g} w) = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w)$
124	121 123	eqeq12d	$⊢ g = W \to ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \leftrightarrow (q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w))$
125	91	fveq2d	$⊢ g = W \to 1_{Scalar (g)} = 1_{F}$
126	125 9	eqtr4di	$⊢ g = W \to 1_{Scalar (g)} = \underset{˙}{1}$
127	98 126 112	oveq123d	$⊢ g = W \to 1_{Scalar (g)} \cdot_{g} w = \underset{˙}{1} \underset{˙}{\cdot} w$
128	127	eqeq1d	$⊢ g = W \to (1_{Scalar (g)} \cdot_{g} w = w \leftrightarrow \underset{˙}{1} \underset{˙}{\cdot} w = w)$
129	91	fveq2d	$⊢ g = W \to 0_{Scalar (g)} = 0_{F}$
130	129 10	eqtr4di	$⊢ g = W \to 0_{Scalar (g)} = O$
131	98 130 112	oveq123d	$⊢ g = W \to 0_{Scalar (g)} \cdot_{g} w = O \underset{˙}{\cdot} w$
132		fveq2	$⊢ g = W \to 0_{g} = 0_{W}$
133	132 4	eqtr4di	$⊢ g = W \to 0_{g} = \underset{˙}{0}$
134	131 133	eqeq12d	$⊢ g = W \to (0_{Scalar (g)} \cdot_{g} w = 0_{g} \leftrightarrow O \underset{˙}{\cdot} w = \underset{˙}{0})$
135	124 128 134	3anbi123d	$⊢ g = W \to (((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g}) \leftrightarrow ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0}))$
136	117 135	anbi12d	$⊢ g = W \to (((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})) \leftrightarrow ((r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)) \land ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0})))$
137	96 136	raleqbidv	$⊢ g = W \to (\forall w \in {Base}_{g} ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})) \leftrightarrow \forall w \in V ((r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)) \land ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0})))$
138	96 137	raleqbidv	$⊢ g = W \to (\forall x \in {Base}_{g} \forall w \in {Base}_{g} ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})) \leftrightarrow \forall x \in V \forall w \in V ((r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)) \land ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0})))$
139	94 138	raleqbidv	$⊢ g = W \to (\forall r \in {Base}_{Scalar (g)} \forall x \in {Base}_{g} \forall w \in {Base}_{g} ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})) \leftrightarrow \forall r \in K \forall x \in V \forall w \in V ((r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)) \land ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0})))$
140	94 139	raleqbidv	$⊢ g = W \to (\forall q \in {Base}_{Scalar (g)} \forall r \in {Base}_{Scalar (g)} \forall x \in {Base}_{g} \forall w \in {Base}_{g} ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g})) \leftrightarrow \forall q \in K \forall r \in K \forall x \in V \forall w \in V ((r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)) \land ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0})))$
141	92 140	anbi12d	$⊢ g = W \to ((Scalar (g) \in SRing \land \forall q \in {Base}_{Scalar (g)} \forall r \in {Base}_{Scalar (g)} \forall x \in {Base}_{g} \forall w \in {Base}_{g} ((r \cdot_{g} w \in {Base}_{g} \land r \cdot_{g} (w +_{g} x) = (r \cdot_{g} w) +_{g} (r \cdot_{g} x) \land (q +_{Scalar (g)} r) \cdot_{g} w = (q \cdot_{g} w) +_{g} (r \cdot_{g} w)) \land ((q \cdot_{Scalar (g)} r) \cdot_{g} w = q \cdot_{g} (r \cdot_{g} w) \land 1_{Scalar (g)} \cdot_{g} w = w \land 0_{Scalar (g)} \cdot_{g} w = 0_{g}))) \leftrightarrow (F \in SRing \land \forall q \in K \forall r \in K \forall x \in V \forall w \in V ((r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)) \land ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0}))))$
142	89 141	syl5bb	$⊢ g = W \to (\underset{˙}{[} {Base}_{g} / v \underset{˙}{]} \underset{˙}{[} +_{g} / a \underset{˙}{]} \underset{˙}{[} \cdot_{g} / s \underset{˙}{]} \underset{˙}{[} Scalar (g) / f \underset{˙}{]} \underset{˙}{[} {Base}_{f} / k \underset{˙}{]} \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} (f \in SRing \land \forall q \in k \forall r \in k \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \land ((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g}))) \leftrightarrow (F \in SRing \land \forall q \in K \forall r \in K \forall x \in V \forall w \in V ((r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)) \land ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0}))))$
143		df-slmd	$⊢ SLMod = \{g \in CMnd \| \underset{˙}{[} {Base}_{g} / v \underset{˙}{]} \underset{˙}{[} +_{g} / a \underset{˙}{]} \underset{˙}{[} \cdot_{g} / s \underset{˙}{]} \underset{˙}{[} Scalar (g) / f \underset{˙}{]} \underset{˙}{[} {Base}_{f} / k \underset{˙}{]} \underset{˙}{[} +_{f} / p \underset{˙}{]} \underset{˙}{[} \cdot_{f} / t \underset{˙}{]} (f \in SRing \land \forall q \in k \forall r \in k \forall x \in v \forall w \in v ((r s w \in v \land r s (w a x) = (r s w) a (r s x) \land (q p r) s w = (q s w) a (r s w)) \land ((q t r) s w = q s (r s w) \land 1_{f} s w = w \land 0_{f} s w = 0_{g})))\}$
144	142 143	elrab2	$⊢ W \in SLMod \leftrightarrow (W \in CMnd \land (F \in SRing \land \forall q \in K \forall r \in K \forall x \in V \forall w \in V ((r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)) \land ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0}))))$
145		3anass	$⊢ (W \in CMnd \land F \in SRing \land \forall q \in K \forall r \in K \forall x \in V \forall w \in V ((r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)) \land ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0}))) \leftrightarrow (W \in CMnd \land (F \in SRing \land \forall q \in K \forall r \in K \forall x \in V \forall w \in V ((r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)) \land ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0}))))$
146	144 145	bitr4i	$⊢ W \in SLMod \leftrightarrow (W \in CMnd \land F \in SRing \land \forall q \in K \forall r \in K \forall x \in V \forall w \in V ((r \underset{˙}{\cdot} w \in V \land r \underset{˙}{\cdot} (w \underset{˙}{+} x) = (r \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} x) \land (q \underset{˙}{⨣} r) \underset{˙}{\cdot} w = (q \underset{˙}{\cdot} w) \underset{˙}{+} (r \underset{˙}{\cdot} w)) \land ((q \underset{˙}{\times} r) \underset{˙}{\cdot} w = q \underset{˙}{\cdot} (r \underset{˙}{\cdot} w) \land \underset{˙}{1} \underset{˙}{\cdot} w = w \land O \underset{˙}{\cdot} w = \underset{˙}{0})))$

Metamath Proof Explorer

Theorem isslmd

Proof