# Metamath Proof Explorer

## Theorem assapropd

Description: If two structures have the same components (properties), one is an associative algebra iff the other one is. (Contributed by Mario Carneiro, 8-Feb-2015)

Ref Expression
Hypotheses assapropd.1 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
assapropd.2 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{L}}$
assapropd.3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{+}_{{K}}{y}={x}{+}_{{L}}{y}$
assapropd.4 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{K}}{y}={x}{\cdot }_{{L}}{y}$
assapropd.5 ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({K}\right)$
assapropd.6 ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({L}\right)$
assapropd.7 ${⊢}{P}={\mathrm{Base}}_{{F}}$
assapropd.8 ${⊢}\left({\phi }\wedge \left({x}\in {P}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{K}}{y}={x}{\cdot }_{{L}}{y}$
Assertion assapropd ${⊢}{\phi }\to \left({K}\in \mathrm{AssAlg}↔{L}\in \mathrm{AssAlg}\right)$

### Proof

Step Hyp Ref Expression
1 assapropd.1 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{K}}$
2 assapropd.2 ${⊢}{\phi }\to {B}={\mathrm{Base}}_{{L}}$
3 assapropd.3 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{+}_{{K}}{y}={x}{+}_{{L}}{y}$
4 assapropd.4 ${⊢}\left({\phi }\wedge \left({x}\in {B}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{K}}{y}={x}{\cdot }_{{L}}{y}$
5 assapropd.5 ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({K}\right)$
6 assapropd.6 ${⊢}{\phi }\to {F}=\mathrm{Scalar}\left({L}\right)$
7 assapropd.7 ${⊢}{P}={\mathrm{Base}}_{{F}}$
8 assapropd.8 ${⊢}\left({\phi }\wedge \left({x}\in {P}\wedge {y}\in {B}\right)\right)\to {x}{\cdot }_{{K}}{y}={x}{\cdot }_{{L}}{y}$
9 assalmod ${⊢}{K}\in \mathrm{AssAlg}\to {K}\in \mathrm{LMod}$
10 assaring ${⊢}{K}\in \mathrm{AssAlg}\to {K}\in \mathrm{Ring}$
11 9 10 jca ${⊢}{K}\in \mathrm{AssAlg}\to \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)$
12 11 a1i ${⊢}{\phi }\to \left({K}\in \mathrm{AssAlg}\to \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)$
13 assalmod ${⊢}{L}\in \mathrm{AssAlg}\to {L}\in \mathrm{LMod}$
14 1 2 3 5 6 7 8 lmodpropd ${⊢}{\phi }\to \left({K}\in \mathrm{LMod}↔{L}\in \mathrm{LMod}\right)$
15 13 14 syl5ibr ${⊢}{\phi }\to \left({L}\in \mathrm{AssAlg}\to {K}\in \mathrm{LMod}\right)$
16 assaring ${⊢}{L}\in \mathrm{AssAlg}\to {L}\in \mathrm{Ring}$
17 1 2 3 4 ringpropd ${⊢}{\phi }\to \left({K}\in \mathrm{Ring}↔{L}\in \mathrm{Ring}\right)$
18 16 17 syl5ibr ${⊢}{\phi }\to \left({L}\in \mathrm{AssAlg}\to {K}\in \mathrm{Ring}\right)$
19 15 18 jcad ${⊢}{\phi }\to \left({L}\in \mathrm{AssAlg}\to \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)$
20 5 6 eqtr3d ${⊢}{\phi }\to \mathrm{Scalar}\left({K}\right)=\mathrm{Scalar}\left({L}\right)$
21 20 eleq1d ${⊢}{\phi }\to \left(\mathrm{Scalar}\left({K}\right)\in \mathrm{CRing}↔\mathrm{Scalar}\left({L}\right)\in \mathrm{CRing}\right)$
22 14 17 21 3anbi123d ${⊢}{\phi }\to \left(\left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\wedge \mathrm{Scalar}\left({K}\right)\in \mathrm{CRing}\right)↔\left({L}\in \mathrm{LMod}\wedge {L}\in \mathrm{Ring}\wedge \mathrm{Scalar}\left({L}\right)\in \mathrm{CRing}\right)\right)$
23 22 adantr ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to \left(\left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\wedge \mathrm{Scalar}\left({K}\right)\in \mathrm{CRing}\right)↔\left({L}\in \mathrm{LMod}\wedge {L}\in \mathrm{Ring}\wedge \mathrm{Scalar}\left({L}\right)\in \mathrm{CRing}\right)\right)$
24 simpll ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {\phi }$
25 simplrl ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {K}\in \mathrm{LMod}$
26 simprl ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {r}\in {P}$
27 5 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}={\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}$
28 7 27 syl5eq ${⊢}{\phi }\to {P}={\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}$
29 24 28 syl ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {P}={\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}$
30 26 29 eleqtrd ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}$
31 simprrl ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {z}\in {B}$
32 24 1 syl ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {B}={\mathrm{Base}}_{{K}}$
33 31 32 eleqtrd ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {z}\in {\mathrm{Base}}_{{K}}$
34 eqid ${⊢}{\mathrm{Base}}_{{K}}={\mathrm{Base}}_{{K}}$
35 eqid ${⊢}\mathrm{Scalar}\left({K}\right)=\mathrm{Scalar}\left({K}\right)$
36 eqid ${⊢}{\cdot }_{{K}}={\cdot }_{{K}}$
37 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}$
38 34 35 36 37 lmodvscl ${⊢}\left({K}\in \mathrm{LMod}\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}\wedge {z}\in {\mathrm{Base}}_{{K}}\right)\to {r}{\cdot }_{{K}}{z}\in {\mathrm{Base}}_{{K}}$
39 25 30 33 38 syl3anc ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {r}{\cdot }_{{K}}{z}\in {\mathrm{Base}}_{{K}}$
40 39 32 eleqtrrd ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {r}{\cdot }_{{K}}{z}\in {B}$
41 simprrr ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {w}\in {B}$
42 4 oveqrspc2v ${⊢}\left({\phi }\wedge \left({r}{\cdot }_{{K}}{z}\in {B}\wedge {w}\in {B}\right)\right)\to \left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}=\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{L}}{w}$
43 24 40 41 42 syl12anc ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to \left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}=\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{L}}{w}$
44 8 oveqrspc2v ${⊢}\left({\phi }\wedge \left({r}\in {P}\wedge {z}\in {B}\right)\right)\to {r}{\cdot }_{{K}}{z}={r}{\cdot }_{{L}}{z}$
45 24 26 31 44 syl12anc ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {r}{\cdot }_{{K}}{z}={r}{\cdot }_{{L}}{z}$
46 45 oveq1d ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to \left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{L}}{w}=\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}$
47 43 46 eqtrd ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to \left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}=\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}$
48 simplrr ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {K}\in \mathrm{Ring}$
49 41 32 eleqtrd ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {w}\in {\mathrm{Base}}_{{K}}$
50 eqid ${⊢}{\cdot }_{{K}}={\cdot }_{{K}}$
51 34 50 ringcl ${⊢}\left({K}\in \mathrm{Ring}\wedge {z}\in {\mathrm{Base}}_{{K}}\wedge {w}\in {\mathrm{Base}}_{{K}}\right)\to {z}{\cdot }_{{K}}{w}\in {\mathrm{Base}}_{{K}}$
52 48 33 49 51 syl3anc ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {z}{\cdot }_{{K}}{w}\in {\mathrm{Base}}_{{K}}$
53 52 32 eleqtrrd ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {z}{\cdot }_{{K}}{w}\in {B}$
54 8 oveqrspc2v ${⊢}\left({\phi }\wedge \left({r}\in {P}\wedge {z}{\cdot }_{{K}}{w}\in {B}\right)\right)\to {r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{K}}{w}\right)$
55 24 26 53 54 syl12anc ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{K}}{w}\right)$
56 4 oveqrspc2v ${⊢}\left({\phi }\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\to {z}{\cdot }_{{K}}{w}={z}{\cdot }_{{L}}{w}$
57 24 31 41 56 syl12anc ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {z}{\cdot }_{{K}}{w}={z}{\cdot }_{{L}}{w}$
58 57 oveq2d ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {r}{\cdot }_{{L}}\left({z}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)$
59 55 58 eqtrd ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)$
60 47 59 eqeq12d ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to \left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)↔\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)$
61 34 35 36 37 lmodvscl ${⊢}\left({K}\in \mathrm{LMod}\wedge {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}\wedge {w}\in {\mathrm{Base}}_{{K}}\right)\to {r}{\cdot }_{{K}}{w}\in {\mathrm{Base}}_{{K}}$
62 25 30 49 61 syl3anc ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {r}{\cdot }_{{K}}{w}\in {\mathrm{Base}}_{{K}}$
63 62 32 eleqtrrd ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {r}{\cdot }_{{K}}{w}\in {B}$
64 4 oveqrspc2v ${⊢}\left({\phi }\wedge \left({z}\in {B}\wedge {r}{\cdot }_{{K}}{w}\in {B}\right)\right)\to {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={z}{\cdot }_{{L}}\left({r}{\cdot }_{{K}}{w}\right)$
65 24 31 63 64 syl12anc ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={z}{\cdot }_{{L}}\left({r}{\cdot }_{{K}}{w}\right)$
66 8 oveqrspc2v ${⊢}\left({\phi }\wedge \left({r}\in {P}\wedge {w}\in {B}\right)\right)\to {r}{\cdot }_{{K}}{w}={r}{\cdot }_{{L}}{w}$
67 24 26 41 66 syl12anc ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {r}{\cdot }_{{K}}{w}={r}{\cdot }_{{L}}{w}$
68 67 oveq2d ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {z}{\cdot }_{{L}}\left({r}{\cdot }_{{K}}{w}\right)={z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)$
69 65 68 eqtrd ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)$
70 69 59 eqeq12d ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to \left({z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)↔{z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)$
71 60 70 anbi12d ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge \left({r}\in {P}\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\right)\to \left(\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)↔\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)\right)$
72 71 anassrs ${⊢}\left(\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge {r}\in {P}\right)\wedge \left({z}\in {B}\wedge {w}\in {B}\right)\right)\to \left(\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)↔\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)\right)$
73 72 2ralbidva ${⊢}\left(\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\wedge {r}\in {P}\right)\to \left(\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)↔\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)\right)$
74 73 ralbidva ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to \left(\forall {r}\in {P}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)↔\forall {r}\in {P}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)\right)$
75 28 adantr ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to {P}={\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}$
76 1 adantr ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to {B}={\mathrm{Base}}_{{K}}$
77 76 raleqdv ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to \left(\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)↔\forall {w}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)\right)$
78 76 77 raleqbidv ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to \left(\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)↔\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)\right)$
79 75 78 raleqbidv ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to \left(\forall {r}\in {P}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)↔\forall {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)\right)$
80 6 fveq2d ${⊢}{\phi }\to {\mathrm{Base}}_{{F}}={\mathrm{Base}}_{\mathrm{Scalar}\left({L}\right)}$
81 7 80 syl5eq ${⊢}{\phi }\to {P}={\mathrm{Base}}_{\mathrm{Scalar}\left({L}\right)}$
82 81 adantr ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to {P}={\mathrm{Base}}_{\mathrm{Scalar}\left({L}\right)}$
83 2 adantr ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to {B}={\mathrm{Base}}_{{L}}$
84 83 raleqdv ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to \left(\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)↔\forall {w}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)\right)$
85 83 84 raleqbidv ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to \left(\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)↔\forall {z}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)\right)$
86 82 85 raleqbidv ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to \left(\forall {r}\in {P}\phantom{\rule{.4em}{0ex}}\forall {z}\in {B}\phantom{\rule{.4em}{0ex}}\forall {w}\in {B}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)↔\forall {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({L}\right)}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)\right)$
87 74 79 86 3bitr3d ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to \left(\forall {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)↔\forall {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({L}\right)}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)\right)$
88 23 87 anbi12d ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to \left(\left(\left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\wedge \mathrm{Scalar}\left({K}\right)\in \mathrm{CRing}\right)\wedge \forall {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)\right)↔\left(\left({L}\in \mathrm{LMod}\wedge {L}\in \mathrm{Ring}\wedge \mathrm{Scalar}\left({L}\right)\in \mathrm{CRing}\right)\wedge \forall {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({L}\right)}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)\right)\right)$
89 34 35 37 36 50 isassa ${⊢}{K}\in \mathrm{AssAlg}↔\left(\left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\wedge \mathrm{Scalar}\left({K}\right)\in \mathrm{CRing}\right)\wedge \forall {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({K}\right)}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{K}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{K}}{z}\right){\cdot }_{{K}}{w}={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\wedge {z}{\cdot }_{{K}}\left({r}{\cdot }_{{K}}{w}\right)={r}{\cdot }_{{K}}\left({z}{\cdot }_{{K}}{w}\right)\right)\right)$
90 eqid ${⊢}{\mathrm{Base}}_{{L}}={\mathrm{Base}}_{{L}}$
91 eqid ${⊢}\mathrm{Scalar}\left({L}\right)=\mathrm{Scalar}\left({L}\right)$
92 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({L}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({L}\right)}$
93 eqid ${⊢}{\cdot }_{{L}}={\cdot }_{{L}}$
94 eqid ${⊢}{\cdot }_{{L}}={\cdot }_{{L}}$
95 90 91 92 93 94 isassa ${⊢}{L}\in \mathrm{AssAlg}↔\left(\left({L}\in \mathrm{LMod}\wedge {L}\in \mathrm{Ring}\wedge \mathrm{Scalar}\left({L}\right)\in \mathrm{CRing}\right)\wedge \forall {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({L}\right)}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{L}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{L}}{z}\right){\cdot }_{{L}}{w}={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\wedge {z}{\cdot }_{{L}}\left({r}{\cdot }_{{L}}{w}\right)={r}{\cdot }_{{L}}\left({z}{\cdot }_{{L}}{w}\right)\right)\right)$
96 88 89 95 3bitr4g ${⊢}\left({\phi }\wedge \left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\right)\to \left({K}\in \mathrm{AssAlg}↔{L}\in \mathrm{AssAlg}\right)$
97 96 ex ${⊢}{\phi }\to \left(\left({K}\in \mathrm{LMod}\wedge {K}\in \mathrm{Ring}\right)\to \left({K}\in \mathrm{AssAlg}↔{L}\in \mathrm{AssAlg}\right)\right)$
98 12 19 97 pm5.21ndd ${⊢}{\phi }\to \left({K}\in \mathrm{AssAlg}↔{L}\in \mathrm{AssAlg}\right)$