isassa

Description: The properties of an associative algebra. (Contributed by Mario Carneiro, 29-Dec-2014) (Revised by SN, 2-Mar-2025)

	Ref	Expression
Hypotheses	isassa.v	$⊢ V = {Base}_{W}$
	isassa.f	$⊢ F = Scalar (W)$
	isassa.b	$⊢ B = {Base}_{F}$
	isassa.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
	isassa.t	$⊢ \underset{˙}{\times} = \cdot_{W}$
Assertion	isassa	$⊢ W \in AssAlg \leftrightarrow ((W \in LMod \land W \in Ring) \land \forall r \in B \forall x \in V \forall y \in V ((r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y) \land x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y)))$

Proof

Step	Hyp	Ref	Expression
1		isassa.v	$⊢ V = {Base}_{W}$
2		isassa.f	$⊢ F = Scalar (W)$
3		isassa.b	$⊢ B = {Base}_{F}$
4		isassa.s	$⊢ \underset{˙}{\cdot} = \cdot_{W}$
5		isassa.t	$⊢ \underset{˙}{\times} = \cdot_{W}$
6		fvexd	$⊢ w = W \to Scalar (w) \in V$
7		fveq2	$⊢ w = W \to Scalar (w) = Scalar (W)$
8	7 2	eqtr4di	$⊢ w = W \to Scalar (w) = F$
9		fveq2	$⊢ f = F \to {Base}_{f} = {Base}_{F}$
10	9 3	eqtr4di	$⊢ f = F \to {Base}_{f} = B$
11	10	adantl	$⊢ (w = W \land f = F) \to {Base}_{f} = B$
12		fveq2	$⊢ w = W \to {Base}_{w} = {Base}_{W}$
13	12 1	eqtr4di	$⊢ w = W \to {Base}_{w} = V$
14		simpr	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to t = \underset{˙}{\times}$
15		simpl	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to s = \underset{˙}{\cdot}$
16	15	oveqd	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to r s x = r \underset{˙}{\cdot} x$
17		eqidd	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to y = y$
18	14 16 17	oveq123d	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to (r s x) t y = (r \underset{˙}{\cdot} x) \underset{˙}{\times} y$
19		eqidd	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to r = r$
20	14	oveqd	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to x t y = x \underset{˙}{\times} y$
21	15 19 20	oveq123d	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to r s (x t y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y)$
22	18 21	eqeq12d	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to ((r s x) t y = r s (x t y) \leftrightarrow (r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y))$
23		eqidd	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to x = x$
24	15	oveqd	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to r s y = r \underset{˙}{\cdot} y$
25	14 23 24	oveq123d	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to x t (r s y) = x \underset{˙}{\times} (r \underset{˙}{\cdot} y)$
26	25 21	eqeq12d	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to (x t (r s y) = r s (x t y) \leftrightarrow x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y))$
27	22 26	anbi12d	$⊢ (s = \underset{˙}{\cdot} \land t = \underset{˙}{\times}) \to (((r s x) t y = r s (x t y) \land x t (r s y) = r s (x t y)) \leftrightarrow ((r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y) \land x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y)))$
28	4 5 27	sbcie2s	$⊢ w = W \to (\underset{˙}{[} \cdot_{w} / s \underset{˙}{]} \underset{˙}{[} \cdot_{w} / t \underset{˙}{]} ((r s x) t y = r s (x t y) \land x t (r s y) = r s (x t y)) \leftrightarrow ((r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y) \land x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y)))$
29	13 28	raleqbidv	$⊢ w = W \to (\forall y \in {Base}_{w} \underset{˙}{[} \cdot_{w} / s \underset{˙}{]} \underset{˙}{[} \cdot_{w} / t \underset{˙}{]} ((r s x) t y = r s (x t y) \land x t (r s y) = r s (x t y)) \leftrightarrow \forall y \in V ((r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y) \land x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y)))$
30	13 29	raleqbidv	$⊢ w = W \to (\forall x \in {Base}_{w} \forall y \in {Base}_{w} \underset{˙}{[} \cdot_{w} / s \underset{˙}{]} \underset{˙}{[} \cdot_{w} / t \underset{˙}{]} ((r s x) t y = r s (x t y) \land x t (r s y) = r s (x t y)) \leftrightarrow \forall x \in V \forall y \in V ((r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y) \land x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y)))$
31	30	adantr	$⊢ (w = W \land f = F) \to (\forall x \in {Base}_{w} \forall y \in {Base}_{w} \underset{˙}{[} \cdot_{w} / s \underset{˙}{]} \underset{˙}{[} \cdot_{w} / t \underset{˙}{]} ((r s x) t y = r s (x t y) \land x t (r s y) = r s (x t y)) \leftrightarrow \forall x \in V \forall y \in V ((r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y) \land x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y)))$
32	11 31	raleqbidv	$⊢ (w = W \land f = F) \to (\forall r \in {Base}_{f} \forall x \in {Base}_{w} \forall y \in {Base}_{w} \underset{˙}{[} \cdot_{w} / s \underset{˙}{]} \underset{˙}{[} \cdot_{w} / t \underset{˙}{]} ((r s x) t y = r s (x t y) \land x t (r s y) = r s (x t y)) \leftrightarrow \forall r \in B \forall x \in V \forall y \in V ((r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y) \land x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y)))$
33	6 8 32	sbcied2	$⊢ w = W \to (\underset{˙}{[} Scalar (w) / f \underset{˙}{]} \forall r \in {Base}_{f} \forall x \in {Base}_{w} \forall y \in {Base}_{w} \underset{˙}{[} \cdot_{w} / s \underset{˙}{]} \underset{˙}{[} \cdot_{w} / t \underset{˙}{]} ((r s x) t y = r s (x t y) \land x t (r s y) = r s (x t y)) \leftrightarrow \forall r \in B \forall x \in V \forall y \in V ((r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y) \land x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y)))$
34		df-assa	$⊢ AssAlg = \{w \in (LMod \cap Ring) \| \underset{˙}{[} Scalar (w) / f \underset{˙}{]} \forall r \in {Base}_{f} \forall x \in {Base}_{w} \forall y \in {Base}_{w} \underset{˙}{[} \cdot_{w} / s \underset{˙}{]} \underset{˙}{[} \cdot_{w} / t \underset{˙}{]} ((r s x) t y = r s (x t y) \land x t (r s y) = r s (x t y))\}$
35	33 34	elrab2	$⊢ W \in AssAlg \leftrightarrow (W \in (LMod \cap Ring) \land \forall r \in B \forall x \in V \forall y \in V ((r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y) \land x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y)))$
36		elin	$⊢ W \in (LMod \cap Ring) \leftrightarrow (W \in LMod \land W \in Ring)$
37	36	anbi1i	$⊢ (W \in (LMod \cap Ring) \land \forall r \in B \forall x \in V \forall y \in V ((r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y) \land x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y))) \leftrightarrow ((W \in LMod \land W \in Ring) \land \forall r \in B \forall x \in V \forall y \in V ((r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y) \land x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y)))$
38	35 37	bitri	$⊢ W \in AssAlg \leftrightarrow ((W \in LMod \land W \in Ring) \land \forall r \in B \forall x \in V \forall y \in V ((r \underset{˙}{\cdot} x) \underset{˙}{\times} y = r \underset{˙}{\cdot} (x \underset{˙}{\times} y) \land x \underset{˙}{\times} (r \underset{˙}{\cdot} y) = r \underset{˙}{\cdot} (x \underset{˙}{\times} y)))$

Metamath Proof Explorer

Theorem isassa

Proof