Theorem asclpropd

Description: If two structures have the same components (properties), one is an associative algebra iff the other one is. The last hypotheses on 1r can be discharged either by letting W = _V (if strong equality is known on .s ) or assuming K is a ring. (Contributed by Mario Carneiro, 5-Jul-2015)

	Ref	Expression
Hypotheses	asclpropd.f	$$⊢F=\mathrm{Scalar}\left(K\right)$$
	asclpropd.g	$$⊢G=\mathrm{Scalar}\left(L\right)$$
	asclpropd.1	$$⊢\phi \to P={\mathrm{Base}}_F$$
	asclpropd.2	$$⊢\phi \to P={\mathrm{Base}}_G$$
	asclpropd.3	$$⊢\left(\phi \wedge \left(x\in P\wedge y\in W\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
	asclpropd.4	$$⊢\phi \to 1_K=1_L$$
	asclpropd.5	$$⊢\phi \to 1_K\in W$$
Assertion	asclpropd	$$⊢\phi \to \mathrm{algSc}\left(K\right)=\mathrm{algSc}\left(L\right)$$

Proof

Step	Hyp	Ref	Expression
1		asclpropd.f	$$⊢F=\mathrm{Scalar}\left(K\right)$$
2		asclpropd.g	$$⊢G=\mathrm{Scalar}\left(L\right)$$
3		asclpropd.1	$$⊢\phi \to P={\mathrm{Base}}_F$$
4		asclpropd.2	$$⊢\phi \to P={\mathrm{Base}}_G$$
5		asclpropd.3	$$⊢\left(\phi \wedge \left(x\in P\wedge y\in W\right)\right)\to x{\cdot }_{K}y=x{\cdot }_{L}y$$
6		asclpropd.4	$$⊢\phi \to 1_K=1_L$$
7		asclpropd.5	$$⊢\phi \to 1_K\in W$$
8	5	oveqrspc2v	$$⊢\left(\phi \wedge \left(z\in P\wedge 1_K\in W\right)\right)\to z{\cdot }_K{1}_K=z{\cdot }_L{1}_K$$
9	8	anassrs	$$⊢\left(\left(\phi \wedge z\in P\right)\wedge 1_K\in W\right)\to z{\cdot }_K{1}_K=z{\cdot }_L{1}_K$$
10	7 9	mpidan	$$⊢\left(\phi \wedge z\in P\right)\to z{\cdot }_K{1}_K=z{\cdot }_L{1}_K$$
11	6	oveq2d	$$⊢\phi \to z{\cdot }_L{1}_K=z{\cdot }_L{1}_L$$
12	11	adantr	$$⊢\left(\phi \wedge z\in P\right)\to z{\cdot }_L{1}_K=z{\cdot }_L{1}_L$$
13	10 12	eqtrd	$$⊢\left(\phi \wedge z\in P\right)\to z{\cdot }_K{1}_K=z{\cdot }_L{1}_L$$
14	13	mpteq2dva	$$⊢\phi \to \left(z\in P⟼z{\cdot }_K{1}_K\right)=\left(z\in P⟼z{\cdot }_L{1}_L\right)$$
15	3	mpteq1d	$$⊢\phi \to \left(z\in P⟼z{\cdot }_K{1}_K\right)=\left(z\in {\mathrm{Base}}_F⟼z{\cdot }_K{1}_K\right)$$
16	4	mpteq1d	$$⊢\phi \to \left(z\in P⟼z{\cdot }_L{1}_L\right)=\left(z\in {\mathrm{Base}}_G⟼z{\cdot }_L{1}_L\right)$$
17	14 15 16	3eqtr3d	$$⊢\phi \to \left(z\in {\mathrm{Base}}_F⟼z{\cdot }_K{1}_K\right)=\left(z\in {\mathrm{Base}}_G⟼z{\cdot }_L{1}_L\right)$$
18		eqid	$$⊢\mathrm{algSc}\left(K\right)=\mathrm{algSc}\left(K\right)$$
19		eqid	$$⊢{\mathrm{Base}}_F={\mathrm{Base}}_F$$
20		eqid	$$⊢{\cdot }_K={\cdot }_K$$
21		eqid	$$⊢1_K=1_K$$
22	18 1 19 20 21	asclfval	$$⊢\mathrm{algSc}\left(K\right)=\left(z\in {\mathrm{Base}}_F⟼z{\cdot }_K{1}_K\right)$$
23		eqid	$$⊢\mathrm{algSc}\left(L\right)=\mathrm{algSc}\left(L\right)$$
24		eqid	$$⊢{\mathrm{Base}}_G={\mathrm{Base}}_G$$
25		eqid	$$⊢{\cdot }_L={\cdot }_L$$
26		eqid	$$⊢1_L=1_L$$
27	23 2 24 25 26	asclfval	$$⊢\mathrm{algSc}\left(L\right)=\left(z\in {\mathrm{Base}}_G⟼z{\cdot }_L{1}_L\right)$$
28	17 22 27	3eqtr4g	$$⊢\phi \to \mathrm{algSc}\left(K\right)=\mathrm{algSc}\left(L\right)$$