Theorem isassad

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

	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.3	$$⊢\phi \to F\in \mathrm{CRing}$$
	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.3	$$⊢\phi \to F\in \mathrm{CRing}$$
9		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)$$
10		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)$$
11	2 8	eqeltrrd	$$⊢\phi \to \mathrm{Scalar}\left(W\right)\in \mathrm{CRing}$$
12	6 7 11	3jca	$$⊢\phi \to \left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\wedge \mathrm{Scalar}\left(W\right)\in \mathrm{CRing}\right)$$
13	9 10	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)$$
14	13	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)$$
15	2	fveq2d	$$⊢\phi \to {\mathrm{Base}}_F={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
16	3 15	eqtrd	$$⊢\phi \to B={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
17	4	oveqd	$$⊢\phi \to r\underset{\dot{}}{·}x=r{\cdot }_{W}x$$
18		eqidd	$$⊢\phi \to y=y$$
19	5 17 18	oveq123d	$$⊢\phi \to \left(r\underset{\dot{}}{·}x\right)\underset{\dot{}}{\times }y=\left(r{\cdot }_{W}x\right){\cdot }_{W}y$$
20		eqidd	$$⊢\phi \to r=r$$
21	5	oveqd	$$⊢\phi \to x\underset{\dot{}}{\times }y=x{\cdot }_{W}y$$
22	4 20 21	oveq123d	$$⊢\phi \to r\underset{\dot{}}{·}\left(x\underset{\dot{}}{\times }y\right)=r{\cdot }_W\left(x{\cdot }_{W}y\right)$$
23	19 22	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)$$
24		eqidd	$$⊢\phi \to x=x$$
25	4	oveqd	$$⊢\phi \to r\underset{\dot{}}{·}y=r{\cdot }_{W}y$$
26	5 24 25	oveq123d	$$⊢\phi \to x\underset{\dot{}}{\times }\left(r\underset{\dot{}}{·}y\right)=x{\cdot }_W\left(r{\cdot }_{W}y\right)$$
27	26 22	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)$$
28	23 27	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)$$
29	1 28	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)$$
30	1 29	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)$$
31	16 30	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)$$
32	14 31	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)$$
33		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
34		eqid	$$⊢\mathrm{Scalar}\left(W\right)=\mathrm{Scalar}\left(W\right)$$
35		eqid	$$⊢{\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}$$
36		eqid	$$⊢{\cdot }_W={\cdot }_W$$
37		eqid	$$⊢{\cdot }_W={\cdot }_W$$
38	33 34 35 36 37	isassa	$$⊢W\in \mathrm{AssAlg}\leftrightarrow \left(\left(W\in \mathrm{LMod}\wedge W\in \mathrm{Ring}\wedge \mathrm{Scalar}\left(W\right)\in \mathrm{CRing}\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)$$
39	12 32 38	sylanbrc	$$⊢\phi \to W\in \mathrm{AssAlg}$$