# Metamath Proof Explorer

## 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)$