Theorem isassad

Description: Sufficient condition for being an associative algebra. (Contributed by Mario Carneiro, 5-Dec-2014) (Revised by SN, 2-Mar-2025)

	Ref	Expression
Hypotheses	isassad.v	$$⊢\phi \to V={\mathrm{Base}}_W$$
	isassad.f	$$⊢\phi \to F=\mathrm{Scalar}\left(W\right)$$
	isassad.b	$$⊢\phi \to B={\mathrm{Base}}_F$$
	isassad.s	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_W$$
	isassad.t	$$⊢\phi \to \underset{\dot{}}{\times }={\cdot }_W$$
	isassad.1	$$⊢\phi \to W\in \mathrm{LMod}$$
	isassad.2	$$⊢\phi \to W\in \mathrm{Ring}$$
	isassad.4	$$⊢\left(\phi \wedge \left(r\in B\wedge x\in V\wedge y\in V\right)\right)\to \left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)$$
	isassad.5	$$⊢\left(\phi \wedge \left(r\in B\wedge x\in V\wedge y\in V\right)\right)\to x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)$$
Assertion	isassad	$$⊢\phi \to W\in \mathrm{AssAlg}$$

Proof

Step	Hyp	Ref	Expression
1		isassad.v	$$⊢\phi \to V={\mathrm{Base}}_W$$
2		isassad.f	$$⊢\phi \to F=\mathrm{Scalar}\left(W\right)$$
3		isassad.b	$$⊢\phi \to B={\mathrm{Base}}_F$$
4		isassad.s	$$⊢\phi \to \underset{\dot{}}{·}={\cdot }_W$$
5		isassad.t	$$⊢\phi \to \underset{\dot{}}{\times }={\cdot }_W$$
6		isassad.1	$$⊢\phi \to W\in \mathrm{LMod}$$
7		isassad.2	$$⊢\phi \to W\in \mathrm{Ring}$$
8		isassad.4	$$⊢\left(\phi \wedge \left(r\in B\wedge x\in V\wedge y\in V\right)\right)\to \left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)$$
9		isassad.5	$$⊢\left(\phi \wedge \left(r\in B\wedge x\in V\wedge y\in V\right)\right)\to x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)$$
10	6 7	jca	$$⊢\phi \to \left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\right)$$
11	8 9	jca	$$⊢\left(\phi \wedge \left(r\in B\wedge x\in V\wedge y\in V\right)\right)\to \left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)$$
12	11	ralrimivvva	$$⊢\phi \to \forall r\in B\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)$$
13	2	fveq2d	$$⊢\phi \to {\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
14	3 13	eqtrd	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
15	4	oveqd	$$⊢\phi \to r\underset{\dot{}}{·}x=r{\cdot }_{W}x$$
16		eqidd	$$⊢\phi \to y=y$$
17	5 15 16	oveq123d	$$⊢\phi \to \left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=\left(r{\cdot }_{W}x\right){\cdot }_{W}y$$
18		eqidd	$$⊢\phi \to r=r$$
19	5	oveqd	$$⊢\phi \to x\underset{\dot{}}{\times }y=x{\cdot }_{W}y$$
20	4 18 19	oveq123d	$$⊢\phi \to r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)=r{\cdot }_W\left(x{\cdot }_{W}y\right)$$
21	17 20	eqeq12d	$$⊢\phi \to \left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\leftrightarrow \left(r{\cdot }_{W}x\right){\cdot }_{W}y=r{\cdot }_W\left(x{\cdot }_{W}y\right)\right)$$
22		eqidd	$$⊢\phi \to x=x$$
23	4	oveqd	$$⊢\phi \to r\underset{\dot{}}{·}y=r{\cdot }_{W}y$$
24	5 22 23	oveq123d	$$⊢\phi \to x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=x{\cdot }_W\left(r{\cdot }_{W}y\right)$$
25	24 20	eqeq12d	$$⊢\phi \to \left(x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\leftrightarrow x{\cdot }_W\left(r{\cdot }_{W}y\right)=r{\cdot }_W\left(x{\cdot }_{W}y\right)\right)$$
26	21 25	anbi12d	$$⊢\phi \to \left(\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\leftrightarrow \left(\left(r{\cdot }_{W}x\right){\cdot }_{W}y=r{\cdot }_W\left(x{\cdot }_{W}y\right)\wedge x{\cdot }_W\left(r{\cdot }_{W}y\right)=r{\cdot }_W\left(x{\cdot }_{W}y\right)\right)\right)$$
27	1 26	raleqbidv	$$⊢\phi \to \left(\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\leftrightarrow \forall y\in {\mathrm{Base}}_W\left(\left(r{\cdot }_{W}x\right){\cdot }_{W}y=r{\cdot }_W\left(x{\cdot }_{W}y\right)\wedge x{\cdot }_W\left(r{\cdot }_{W}y\right)=r{\cdot }_W\left(x{\cdot }_{W}y\right)\right)\right)$$
28	1 27	raleqbidv	$$⊢\phi \to \left(\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\leftrightarrow \forall x\in {\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_W\left(\left(r{\cdot }_{W}x\right){\cdot }_{W}y=r{\cdot }_W\left(x{\cdot }_{W}y\right)\wedge x{\cdot }_W\left(r{\cdot }_{W}y\right)=r{\cdot }_W\left(x{\cdot }_{W}y\right)\right)\right)$$
29	14 28	raleqbidv	$$⊢\phi \to \left(\forall r\in B\forall x\in V\forall y\in V\left(\left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\wedge x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)\right)\leftrightarrow \forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall x\in {\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_W\left(\left(r{\cdot }_{W}x\right){\cdot }_{W}y=r{\cdot }_W\left(x{\cdot }_{W}y\right)\wedge x{\cdot }_W\left(r{\cdot }_{W}y\right)=r{\cdot }_W\left(x{\cdot }_{W}y\right)\right)\right)$$
30	12 29	mpbid	$$⊢\phi \to \forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall x\in {\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_W\left(\left(r{\cdot }_{W}x\right){\cdot }_{W}y=r{\cdot }_W\left(x{\cdot }_{W}y\right)\wedge x{\cdot }_W\left(r{\cdot }_{W}y\right)=r{\cdot }_W\left(x{\cdot }_{W}y\right)\right)$$
31		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
32		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
33		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
34		eqid	$$⊢{\cdot }_W={\cdot }_W$$
35		eqid	$$⊢{\cdot }_W={\cdot }_W$$
36	31 32 33 34 35	isassa	$$⊢W\in \mathrm{AssAlg}\leftrightarrow \left(\left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\right)\wedge \forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall x\in {\mathrm{Base}}_W\forall y\in {\mathrm{Base}}_W\left(\left(r{\cdot }_{W}x\right){\cdot }_{W}y=r{\cdot }_W\left(x{\cdot }_{W}y\right)\wedge x{\cdot }_W\left(r{\cdot }_{W}y\right)=r{\cdot }_W\left(x{\cdot }_{W}y\right)\right)\right)$$
37	10 30 36	sylanbrc	$$⊢\phi \to W\in \mathrm{AssAlg}$$